Octobre 2018 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][report/itd] -
by Stefan 31 Oct '18

31 Oct '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: 5225f4b5 by Stefan Monnier at 2018-10-31T15:05:17Z - - - - - - 2 changed files: - .gitignore - paper.tex Changes: ===================================== .gitignore ===================================== @@ -16,6 +16,13 @@ manual.?? *.info comment.cut +# llncs2e's other files, not needed to build the article +llncs2e/fig1.eps +llncs2e/history.txt +llncs2e/readme.txt +llncs2e/samplepaper.tex +llncs2e/splncs04.bst + *_build/ # Random backup/autosave files ===================================== paper.tex ===================================== @@ -156,7 +156,7 @@ presentation of CIC's inductive types where the various elements are provided separately, such that inductive types are built on top of tuples and sums rather than the other way around. The resulting language is - lower-level yet we show it to be equivalent to (a predicative version of) + lower-level yet we show it to be equivalent to a predicative version of the Calculus of Inductive Constructions. An additional benefit is that it can conveniently give a precise type to the default branch of \kw{case} statements. @@ -251,8 +251,8 @@ The contributions of this article are: \item A kind of case-analysis construct where the default branch also gets refined type information witnessing in an efficient way precise information about the branches already tested. -\item A proof of equivalence of this language with (a predicative version - of) the Calculus of Inductive Constructions. +\item A proof of equivalence of this language with a predicative version + of the Calculus of Inductive Constructions. \end{itemize} \section{Background} @@ -407,6 +407,7 @@ it practical to provide this feature even if it is not used very often. \textsl{(level)} & \ell &\in& \mathbb{N} \\ \textsl{(ctxt)} & \Gamma,\Delta &::=& \EmptyCtx ~|~ \Gamma,x\:\tau \\ \textsl{(sort)} & s &::=& \Type \ell \\ + %% FIXME: Already give the full syntax here! \textsl{(term)} & e,\tau &::=& s ~|~ x ~|~ \Tlam x \tau e ~|~ \Tapp{e_1}{e_2} ~|~ \Tarw x {\tau_1} {\tau_2} \end{array} @@ -471,6 +472,10 @@ Figure~\ref{fig:ccw} shows our base language \CCw{} as a pure type system (PTS)~\cite{Barendregt91b}. It is a variant of CoC with a tower of universes à la ECC~\cite{Luo89}. +%% FIXME: The issue is much more serious, since impredicativity almost +%% ends up introducing restrictions which prevent defining π₁ and/or π₂ +%% on impredicative sums, so it's far from clear how to turn a `case` into +%% a switch+projections in such a case! While inductive types have non-trivial interactions with impredicativity, those interactions are largely orthogonal to our work, so contrary to most other presentations, we did not include an impredicative universe at the @@ -569,7 +574,7 @@ reduction rule for CUC resp.~CIC. \begin{figure} %% \begin{displaymath} - %% %% FIXME: `Tnth` isn't be a function since it's only defined if + %% %% FIXME: `Tnth` can't be a function since it's only defined if %% %% the index is within bounds! %% \MAlign{ %% %% FIXME: Mutual recursion, yuck! @@ -938,9 +943,6 @@ be simplified in the erasure semantics presented in Section~\ref{sec:erasure}. -%% FIXME: reduction rules? Especially for the `weaken` thingy! - - \subsection{Recursion} \newcommand \Tmu[4][] {\mu_{#1} #2\:#3 . #4} @@ -1237,6 +1239,13 @@ be implemented as no-ops: \section{Equivalence} \label{sec:equivalence} +%% FIXME: We have a problem with inductive types's universe level: CUC +%% does not let the user define Bool elsewhere than Type₀, whereas +%% the CIC presented does. +%% More specifically, in CIC-as-presented, the user can choose the universe +%% level of any Ind type, whereas in CUC-as-presented the user can choose it +%% for types that are recursive but not for those that aren't! + Now that we have defined a calculus which provides us with the intended run-time cost, we show that this calculus is sound and complete with respect to a more classic presentation of inductive types. We will first present @@ -1539,8 +1548,6 @@ in~\cite{Coquand92}: \Ftocic {\Tproj e 0} & \TIproj 1 {\Ftocic {e}} \\ \Ftocic {\Tproj e i} & \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} \\ \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} 0}} & - %% FIXME: We don't have enough type annotations in CUC to - %% fill the type annotations in CIC! \TIcase {\Tlam \_ \_ ?} {e_2} {?} {\Tlam x \tau {\Tlam {x_2} \_ {e_1}}} \\ \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} i}} & @@ -1594,6 +1601,11 @@ $\Jcuc e \bot$ only if there's a $e'$ such that $\Jcic {e'} \bot$, because $\Ftocic \bot = \bot$. \FIXME{Second take:} +%% This is much better, but we need to adjust the presentation accordingly: +%% - We can throw away some type annotations (yay!) +%% - We have to explain that while $\Ftocic\cdot$ is defined on derivations +%% we present it as if it was derived on the syntax of terms, to be +%% more concise. We define a translation function $\Ftocic\cdot$ which takes a derivation $\Jcuc{e}{\tau}$ and returns an equivalent expression $e'$ in CIC. As an abuse @@ -1639,6 +1651,8 @@ If we have $\Jcic e \tau$ then $\Jcuc {\Ftocuc e} {\Ftocuc \tau}$. \section{Extensions} +%% FIXME: Generalize to impredicativity! + The language can be made more general by reifying some of the auxiliary judgments into the logic: \begin{itemize} View it on GitLab: https://gitlab.com/monnier/typer/commit/5225f4b514368cc30a859f80522e16b1567… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/5225f4b514368cc30a859f80522e16b1567… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] Reorder related works; make it fit in 16 pages
by Stefan 29 Oct '18

29 Oct '18

Stefan pushed to branch report/jfla-2019 at Stefan / Typer Commits: eac6b267 by Stefan Monnier at 2018-10-29T20:39:17Z Reorder related works; make it fit in 16 pages - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -121,7 +121,7 @@ The paper presents the following contributions of the design of Typer: \item An elaboration phase which combines HM-style type inference and macro-expansion, relying on the inferred type information to distinguish macro calls. -\item A core language that extends ICC*~\cite{Barras08} with inductive types +\item An extension of ICC*~\cite{Barras08} with inductive types and a new rule for impredicativity. \end{itemize} @@ -168,11 +168,11 @@ To define a new datatype to represent singly linked lists you can write: | cons (hd : a) (tl : List a); \end{verbatim} %% -where \id{hd} and \id{tl} are field names. We could have written just -\verb+cons a (List a)+ instead to keep the fields anonymous. - +where \id{hd} and \id{tl} are optional field names: we could have written just +\verb+cons a (List a)+ instead. +%% Functions and data constructors are curried. You can define the -traditional \id{map} function as follows: +\id{map} function as follows: \begin{verbatim} map : (a : Type) ⇛ (b : Type) ⇛ (a -> b) -> List a -> List b; @@ -264,7 +264,7 @@ that monad. \label{sec:syntax} \newcommand \FigTyperSexp { - \begin{figure}[b] + \begin{figure} \begin{displaymath} \MAlign{ \kw{type}~\id{Sexp} \\ @@ -278,7 +278,6 @@ that monad. \label{fig:Typer-Sexp} \end{figure} } -\FigTyperSexp Once lexical analysis is performed, rather than performing the syntactic analysis in one step, Typer further subdivides the syntactic analysis phase @@ -291,6 +290,8 @@ will produce the same \id{Sexp} as just \texttt{x}. And we use \texttt{()} as the printed representation of the zero-length \id{symbol} (which we call \emph{espilon}). +\FigTyperSexp + Note how, at this stage, the representation of the code has no notion of bindings, functions, types, or function calls. It's only in a second step that S-expressions are analyzed to distinguish the various constructs such @@ -298,7 +299,7 @@ as macro calls, function calls, \kw{let} bindings, variable references, etc. Any S-expression written using an infix or mixfix operator can also be written some other way, following the underscore convention of Agda's -mixfix~\cite{Danielsson08}. In the case of Typer, instead of writing +mixfix~\cite{Danielsson08}. In the case of Typer, instead of: \begin{verbatim} let x = a * b + c in x \end{verbatim} @@ -340,7 +341,7 @@ Then it will consider ``\texttt{+ (f(5) * 6) -}'' and add an open paren: ... g + ((f(5) * 6) - x ... \end{verbatim} and so on and so forth. What sets OPG apart here is that it makes these -choices without considering $e$ nor the surrounding context: instead, it +choices without considering $e$ nor the surrounding context: it bases its decision only on the pair of keywords. In Typer, the grammar is represented by simply associating to each keyword @@ -455,10 +456,9 @@ is that macro's definition. %% turns it into an expression in Typer's core $\lambda$-calculus. Elaboration is the phase in Typer's compiler which turns an S-expression -into an expression in Typer's core $\lambda$-calculus. We want a large part of -this phase to be itself implemented in Typer so that we can prove some of -its properties, such as the correctness of the compilation of pattern -matching~\cite{Cockx18}. +into an expression in Typer's core $\lambda$-calculus. We want most of this phase +to be itself implemented in Typer so that we can prove properties such as +the correctness of the compilation of pattern matching~\cite{Cockx18}. Figure~\ref{fig:Lexp} shows the (simplified) representation used internally for that calculus. Notice that \id{Lexp} represents both what is usually @@ -727,11 +727,11 @@ extended with annotations to indicate which arguments are |~ (x\:\tau_1)\TEarw\tau_2 ~|~ \lambda x\:\tau \TEarw e ~|~ \TEapp{e_1}{e_2}} \end{array} \end{displaymath} -Those annotations are similar to those of Bernardy \etal's colored pure type -systems~\cite{Bernardy12}, in that the annotation on a function or function -call has to match the annotation of the function's type. -The rules of the colored pure type system corresponding to Typer's core -calculus are the following: +Those annotations are similar to those of Bernardy \etal's colored PTS +(CPTS)~\cite{Bernardy12}, in that the annotation on a function or function +call has to match the annotation of the function's type. The rules of the +CPTS corresponding to Typer's core calculus are the +following: \begin{displaymath} \begin{array}{lcl} \mathcal{S} &=& \{~ \kw{Type}~\ell ~|~ \ell\in\mathbb{N} ~\} \\ @@ -746,8 +746,14 @@ calculus are the following: } \end{array} \end{displaymath} -%% FIXME: Explain what these S/A/R mean! -But the typing rule we use is slightly different for erasable functions: +Where $\mathcal{S}$ is the set of possible sorts (i.e.~types of types), +$\mathcal{A}$ is the set of axioms, and $\mathcal{R}$ specifies the set of +allowed abstractions: $(k, s_1, s_2, s_3)$ means that an arrow of color +$k$ can go from an argument in sort $s_1$ to a result in sort +$s_2$, and that this arrow will live in sort $s_3$. + +Compared to a normal CPTS, we use a slightly different typing rule for +erasable functions: \begin{displaymath} \Infer{\Jtyper {\tau_1} s \\ \Jtyper[\Gamma,x\:\tau_1] e {\tau_2} \\ @@ -953,14 +959,14 @@ redundant in ICC*. More specifically: \begin{proof} By induction on the derivation of $\Jtyper[\Gamma_e] e {\tau_e}$. Since $\tau_e : \kw{Prop}$, clearly $e$ can neither be a sort nor an arrow type and it - cannot be $x$ itself either, so it can only be either a $\lambda y:\tau_y \to e_y$ or + cannot be $x$ itself either, so it can only be either a $\lambda y\:\tau_y \to e_y$ or an application $e_1~e_2$. We can apply the induction hypothesis to $e_y$ and to $e_1$. As for $e_2$, there are two cases: either $e_1$ takes an argument of type $\tau_1\:\kw{Type}~\ell'$ in which case we're done, or it takes an argument of type $\tau_1\:\kw{Prop}$ in which case we can again apply the induction hypothesis. \end{proof} -Corollary: the rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since +Corollary: ICC*'s rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since we could convert all the impredicative functions that use it to functions that use $(\kw{e}, s, \kw{Prop}, \kw{Prop})$ instead. @@ -975,9 +981,9 @@ this respect weaker than CIC. But Typer is incomparable to CIC because in another respect it allows things that CIC does not. As mentioned before, CIC has a special restriction that large inductive -types (i.e. inductive types that belong to a universe that is smaller than +types (i.e.~inductive types that belong to a universe that is smaller than some of the values it carries) cannot be used in a strong elimination -(i.e. a \kw{case} analysis that returns a type in a universe larger than +(i.e.~a \kw{case} analysis that returns a type in a universe larger than that of the object analyzed). This restriction means for example that while we can define in Coq @@ -988,15 +994,17 @@ a large inductive type like: | arw : Ω -> Ω -> Ω | all : forall k:Set, (k -> Ω) -> Ω. \end{verbatim} -we cannot prove properties such as: +we cannot prove properties such as the following (which we needed +while working on~\cite{Monnier07}): \begin{verbatim} forall K₁ K₂ F₁ F₂ P, all K₁ F₁ = all K₂ F₂ -> P K₁ F₁ -> P K₂ F₂. \end{verbatim} This important restriction significantly reduces the applicability of large -inductive types, but is needed because it would be otherwise possible to -``smuggle'' a large element within an inductive object of a smaller universe -and take it back out later, resulting in unsoundness~\cite{Coquand86b}. +inductive types, but is needed because it would be otherwise possible +to ``smuggle'' a large element within an inductive object of a smaller +universe and take it back out later, resulting in +unsoundness~\cite{Coquand86b}. Since Typer's impredicativity is limited to erasable elements, those large elements cannot really be taken back out later anyway, by virtue of their @@ -1026,16 +1034,7 @@ discussed by Fruchart and Longo in~\cite{Fruchart96}. %% FIXME: re-order! %% FIXME: Shorten, and then add things: -%% F-star? ATS? - - %% - impredicativity and ICC, -%% - the handling of refinement (Zombie) -%% - let-generalizaintion -%% - comparison to template haskell's elaboration -%% - comparison to Idris -%% - comparison to Lean and Idris's elaboration/tacitcs tools - %% \nocite{Miquel01,Barras08} %ICC %% \nocite{Bernardo09} %ICIC @@ -1050,12 +1049,66 @@ predecessors to be able to list them all. We will try and limit ourselves to some recent systems which share enough of their design or their goals here. -\paragraph{Scala} provides sophisticated meta programming~\cite{Burmako13} -and staged computation~\cite{Rompf13} facilities used in novel ways. - -\paragraph{The Star language}\hspace{-10pt}~\cite{McCabe13} is statically +\paragraph{Honu}\hspace{-10pt}~\cite{Rafkind12} is a programming language in +the Racket system which provides an extensible infix/mixfix syntax +integrated with Racket's metaprogramming facilities. +\textbf{Typed Racket}~\cite{Felleisen11} uses an extension +of Scheme's macro system to implement a statically typed variant of Racket +as a sort of embedded DSL, thus implementing the type checker as part of +a macro. It shares with Typer the characteristic of mixing Lisp-style +macros and static typing, and generally the Racket system shares with Typer +the goal of a being a ``language workbench'' on top of which other languages +can easily be defined, Typed Racket and Honu being just some examples. +%% At first look one might see Typer as a dependently typed Typed +%% Racket. Indeed both have a powerful macro system and a static type +%% system. But there are some important differences. The first difference +%% directly related to this article is that Typed Racket lacks built-in +%% support for mixfix. +%% +%% Another important difference is that Typed Racket macros ala Scheme are +%% hygienic while Typer's macros currently do not provide hygiene. +%% %% Typer is still in its infancy and hygienic macros is future work. +%% Also, Typer's macros are intended to work with dependently typed pieces of +%% code and mathematical proofs and thus require access to the type environment +%% at the expansion site. Typed Racket and more generally Scheme macros, on +%% the other hand, do not have access to the lexical environment at the +%% expansion site. +The \textbf{Star} language~\cite{McCabe13} is a statically typed programming language which also makes it easy to define embedded DSLs via syntactic and macro expansion facilities. +\textbf{Scala} also provides sophisticated meta programming~\cite{Burmako13} +and staged computation~\cite{Rompf13} facilities used in novel ways. +\textbf{OCaml} offers extensible syntax and metaprogramming +facilities in various forms, such as via its Camlp4 +system~\cite{de2003camlp4} and more recently with \emph{extension points}, +which work like macros, by mapping OCaml AST to OCaml AST. +%% where the ``P4'' stands for PreProcessor +%% and Pretty-Printer. Much like a macro system, it allows the programmer to +%% describe an extension to the OCaml parser. The job of CamlP4 is to convert +%% those extensions to standard OCaml's AST. The syntax extension is transparent +%% to the programmer. But CamlP4 is a separate tool from the compiler and the +%% drawback of this approach is that, unlike Nemerle or Typer, syntactic +%% extensions do not have access to typing information. +%% This is one of the +%% main reasons why Typer adopts a macro system which is build-in with +%% the compiler. +%% +%% ToDo : Find article/citation for Alain Frisch extension points (if any) +%% Recent versions of OCaml (after version 4.01.0) also come with +%% . The grammar now accepts annotations to the source file and +%% a special construct, extension nodes, for syntax extension. When the +%% compiler encounters an annotated branch in the AST or an extension node in +%% an expression it calls the macro associated with the annotation. Of course, +%% as in the case of Template Haskell, this means that uses of those extensions +%% have to use a special syntax and hence feel like second-class features. +%% +%% In a language like Typer, where the philosophy is to push most +%% constructs out of the compiler and into libraries such method would +%% result in the source file being fully annotated everywhere. For +%% example, \id{if\_then\_else} and many other constructs are part of the +%% OCaml syntax and would require annotation in Typer if we were to use +%% such strategy. We therefore think Typer has hit a sweet spot between +%% Lisp and OCaml. \paragraph{Template Haskell}\hspace{-10pt}~\cite{Sheard02} is an extension of Haskell to allow @@ -1067,15 +1120,23 @@ purely functional language. %% For such purpose, our use of a Typer's interleaving of type inference and macro expansion is very similar to that of Template Haskell. But Typer and Template Haskell differ on how the macros are used by the programmer: in Template Haskell, macro calls are -made explicit in the source file by preceding them with a \$ sign rather +made explicit in the source file by preceding them with a \Char{\$} sign rather than being determined by their type. Also Template Haskell is not meant to add new binding forms to the language: arguments to the macro are type checked before being passed to the macro. +%% -\paragraph{Zombie}\hspace{-10pt}~\cite{Casinghino14} is an experimental +\paragraph{Idris}\hspace{-10pt}~\cite{Brady13} and +\textbf{F-Star}~\cite{Swamy16} are programming languages with dependent +types. They shares many of Typer's goals and also offers metaprogramming +facilities, although these facilities are more aimed at writing proofs, +while Typer's metaprogramming facilities are more currently geared toward +syntactic extensions. +%% +\textbf{Zombie}~\cite{Casinghino14} is an experimental programming language with dependent types. One of its most novel features is to eschew automatic reductions at the type level and require manual cast -operation instead. This is a bit like of Typer's intentionally weak typing +operations instead. This is a bit like of Typer's intentionally weak typing rule for \kw{case}, relying on explicit cast operations using type equality witnesses for type refinement, but pushed yet further. @@ -1086,37 +1147,22 @@ not just infix operators. Their use of mixfix operators like the idea of adding mixfix to S-expressions in Typer using operator precedence grammar. For a more detailed and formal discussion on mixfix operators and Agda, see~\cite{Danielsson08}. - -\paragraph{Idris}\hspace{-10pt}~\cite{Brady13} is a programming language -based on type theory. It shares many of Typer's goals and also offers -metaprogramming facilities. - -\paragraph{Honu}\hspace{-10pt}~\cite{Rafkind12} is a programming language in -the Racket system which provides an extensible infix/mixfix syntax -integrated with Racket's metaprogramming facilities. - -\paragraph{Typed Racket}\hspace{-10pt}~\cite{Felleisen11} uses an extension -of Scheme's macro system to implement a statically typed variant of Racket -as a sort of embedded DSL, thus implementing the type checker as part of -a macro. It shares with Typer the characteristic of mixing Lisp-style -macros and static typing, and generally the Racket system shares with Typer -the goal of a being a ``language workbench'' on top of which other languages -can easily be defined, Typed Racket and Honu being just some examples. - -%% At first look one might see Typer as a dependently typed Typed -%% Racket. Indeed both have a powerful macro system and a static type -%% system. But there are some important differences. The first difference -%% directly related to this article is that Typed Racket lacks built-in -%% support for mixfix. - -%% Another important difference is that Typed Racket macros ala Scheme are -%% hygienic while Typer's macros currently do not provide hygiene. -%% %% Typer is still in its infancy and hygienic macros is future work. -%% Also, Typer's macros are intended to work with dependently typed pieces of -%% code and mathematical proofs and thus require access to the type environment -%% at the expansion site. Typed Racket and more generally Scheme macros, on -%% the other hand, do not have access to the lexical environment at the -%% expansion site. +%% +\textbf{Coq}~\cite{Coq00} has syntactic extensions similar +to mixfix as well as a sophisticated metaprogramming language known as +Ltac~\cite{Delahaye00}. More recently other metaprogramming languages have +been designed for it such as Mtac~\cite{Ziliani13} and Rtac~\cite{Malecha16}. +%% Coq's syntactic +%% extensions, based on CamlP4, are fairly sophisticated. But Coq's +%% metaprogramming language is a separate language that is very different from +%% Coq core language Gallina and you can't directly invoke Ltac tactics from +%% Gallina code. This is a key difference between Coq and Typer. We wish for +%% Typer to have the same language for both purposes as Lisp and Scheme have +%% already demonstrated the benefits of having the same language for both. +%% +%% Nonetheless, it remains to be shown that macros are as user-friendly +%% to automate mathematical proofs as tactics written in Ltac which is a +%% domain specific language tailored for this task. %% \subsection{Dylan} %% Dylan~\cite{Dylan,Backrach99} is a functional and object-oriented @@ -1194,56 +1240,6 @@ can easily be defined, Typed Racket and Honu being just some examples. %% %% to Typer's macros who also have access to the environment at the %% %% expansion site. -\paragraph{OCaml}\hspace{-10pt} offers extensible syntax and metaprogramming -facilities in various forms, such as via its Camlp4 -system~\cite{de2003camlp4} and more recently with \emph{extension points}, -which work like macros, by mapping OCaml AST to OCaml AST. - -%% where the ``P4'' stands for PreProcessor -%% and Pretty-Printer. Much like a macro system, it allows the programmer to -%% describe an extension to the OCaml parser. The job of CamlP4 is to convert -%% those extensions to standard OCaml's AST. The syntax extension is transparent -%% to the programmer. But CamlP4 is a separate tool from the compiler and the -%% drawback of this approach is that, unlike Nemerle or Typer, syntactic -%% extensions do not have access to typing information. -%% This is one of the -%% main reasons why Typer adopts a macro system which is build-in with -%% the compiler. - -%ToDo : Find article/citation for Alain Frisch extension points (if any) -%% Recent versions of OCaml (after version 4.01.0) also come with -%% . The grammar now accepts annotations to the source file and -%% a special construct, extension nodes, for syntax extension. When the -%% compiler encounters an annotated branch in the AST or an extension node in -%% an expression it calls the macro associated with the annotation. Of course, -%% as in the case of Template Haskell, this means that uses of those extensions -%% have to use a special syntax and hence feel like second-class features. - -%% In a language like Typer, where the philosophy is to push most -%% constructs out of the compiler and into libraries such method would -%% result in the source file being fully annotated everywhere. For -%% example, \id{if\_then\_else} and many other constructs are part of the -%% OCaml syntax and would require annotation in Typer if we were to use -%% such strategy. We therefore think Typer has hit a sweet spot between -%% Lisp and OCaml. - -\paragraph{Coq}\hspace{-10pt}~\cite{Coq00} has syntactic extensions similar -to mixfix as well as a sophisticated metaprogramming language known as -Ltac~\cite{Delahaye00}. More recently other metaprogramming languages have -been designed for it such as Mtac~\cite{Ziliani13} and Rtac~\cite{Malecha16}. -%% Coq's syntactic -%% extensions, based on CamlP4, are fairly sophisticated. But Coq's -%% metaprogramming language is a separate language that is very different from -%% Coq core language Gallina and you can't directly invoke Ltac tactics from -%% Gallina code. This is a key difference between Coq and Typer. We wish for -%% Typer to have the same language for both purposes as Lisp and Scheme have -%% already demonstrated the benefits of having the same language for both. - -%% Nonetheless, it remains to be shown that macros are as user-friendly -%% to automate mathematical proofs as tactics written in Ltac which is a -%% domain specific language tailored for this task. - - \section{Conclusion} Typer is a new experimental language in the family of dependently typed View it on GitLab: https://gitlab.com/monnier/typer/commit/eac6b2673a37bf5205774d351930a8b72d6… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/eac6b2673a37bf5205774d351930a8b72d6… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] -
by Stefan 28 Oct '18

28 Oct '18

Stefan pushed to branch report/jfla-2019 at Stefan / Typer Commits: 1347e7b4 by Stefan Monnier at 2018-10-28T22:53:12Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -348,7 +348,22 @@ two precedence levels: one for its left side and another for its right side. Then parsing uses the following rule: when we see ``$\id{kw}_1~e~\id{kw}_2$'', we lookup the right precedence of $\id{kw}_1$ and the left precedence of $\id{kw}_2$, and we then attach $e$ to -whichever is higher. +whichever is higher. If the precedences are equal, then we consider those +two keywords as part of a mixfix. + +For example, given the default grammar, we can define the new form +``$\kw{if}~e_1~\kw{then}~e_2~\kw{else}~e_3$'' by setting the precedences as +follows; +\begin{verbatim} + define-operator "if" () 2; + define-operator "then" 2 1; + define-operator "else" 1 66; +\end{verbatim} +After which such a form gets parsed identically to +``$\id{if\_then\_else\_}~e_1~e_2~e_3$''. Note that the modification of the +grammar is independent from the definition of \id{if\_then\_else\_} as +a macro: the grammar can be changed for infix functions and new macros +can be defined without changing the grammar. While it enjoys a simple and efficient implementation\footnote{as well as some other interesting properties such as the ability to parse backward.} @@ -394,8 +409,6 @@ to an OPG grammar we disallow these context-dependent parsing rules, such that we do not need to know what is a macro call, let alone figure out what is that macro's definition. -%% FIXME: Show how to change the precedence table for if/then/else - \section{Elaboration} \label{sec:elaboration} @@ -655,43 +668,44 @@ specialized (i.e. Typer inserts a type application). HM performs generalization (i.e.~introduction of implicit (type) abstractions) whenever a value is defined in a let-binding. Typer does the -same with the following differences: if the variable had a type annotation, -we don't perform generalization (instead, the bidirectional type checking -propagates the type information into the function so there shouldn't be -anything left to generalize); if the free meta-variable is used in -a non-erasable way, we signal an error since generalizing it with an -erasable abstraction would lead to invalid code. - -%% FIXME: Discuss decidability/termination -%% FIXME: Is it an actual strict superset of HM (I think so, except for -%% the case of recursion where we currently require a type annotation). - -There are two further places where generalization happens: when a $\lambda$ -abstraction is elaborated in a context that expects an erasable function, we -wrap it into an additional erasable $\lambda$; and when elaborating a \emph{type - annotation}, all remaining free meta variables are generalized into -erasable arrows. - -We use the ``\texttt{?}'' prefix for user-written meta-variables, so the +same when the variable had a type annotation, but with the following +difference: if a free meta-variable is used in a non-erasable way, we signal +an error since generalizing it with an erasable abstraction would lead to +invalid code. + +For definitions that come with a type annotation, Typer also provides a form +of generalization: first, when elaborating a \emph{type annotation}, all +remaining free meta variables are generalized into erasable arrows, so the user can write: \begin{verbatim} map : (?a -> ?b) -> List ?a -> List ?b; \end{verbatim} +where we use the ``\texttt{?}'' prefix for user-written meta-variables, so +Typer will add \texttt{?a} and \texttt{?b} as two additional erasable +arguments. %% and this will be elaborated to a type equivalent to: %% \begin{verbatim} %% map : (a : Type) ≡> (b : Type) ≡> %% (a -> b) -> List a -> List b; %% \end{verbatim} -and Typer will add \texttt{?a} and \texttt{?b} as two additional erasable -arguments. This reproduces the same behavior as that used in systems such -as Twelf~\cite{Pfenning99}. After that, when we define +This reproduces the same behavior as that used in systems such as +Twelf~\cite{Pfenning99}. + +Second, when a $\lambda$ abstraction is elaborated in a context that expects an +erasable function, we wrap it into an additional erasable $\lambda$. So if the +previous type annotation is followed by: \begin{verbatim} map f x = ...; \end{verbatim} -it defines \texttt{map} as a normal $\lambda$ abstraction whereas the context -(from the previous type annotation) expects a function with two erasable -arguments, so the elaboration of the $\lambda$ will automatically add the two -additional (erasable) $\lambda$ corresponding to \texttt{?a} and \texttt{?b}. +the elaboration will automatically add the two additional (erasable) $\lambda$ +corresponding to \texttt{?a} and \texttt{?b}. + +We believe this behaves just like HM inference for the corresponding +sublanguage, but have not shown it yet. Also we do not know whether this +inference algorithm is guaranteed to terminate in theory, but it seems to +perform well in practice. Given that macro-expansion is allowed to perform +arbitrary side-effects, we have already given up the idea of guaranteeing +termination of elaboration anyway. \section{Core language} @@ -986,28 +1000,27 @@ and take it back out later, resulting in unsoundness~\cite{Coquand86b}. Since Typer's impredicativity is limited to erasable elements, those large elements cannot really be taken back out later anyway, by virtue of their -erasability. For this reason, we conjecture that our form of +erasability. For this reason, we \emph{conjecture} that our form of impredicativity does not require this restriction on strong elimination. As a consequence, in Typer we can define the above inductive type (with an erasable $k$) and prove its property (again with erasable $K_1$ and $K_2$). -\subsection{Impredicativity rules of Typer} - -%% FIXME: Maybe remove this subsection. - -Once we decided to try our luck with this conjecture, it was a small step to -add yet more potentially risky features to our calculus. So we currently -also allow impredicativity at all universe levels rather than only at the -bottom. Clearly, this risks falling victim of paradoxes like -Hurken's~\cite{Hurkens95}, so buyer beware: we have no yet made any serious -attempt at proving or disproving the soundness of this extension. - The weak justification behind it, is a philosophical one: erasable arguments are not \emph{significant}, so a function that takes an erasable argument could be considered as a mere ``schema'' or ``prototype'' which stands for all the specialized versions of the function. A similar argument is discussed by Fruchart and Longo in~\cite{Fruchart96}. +%% \subsection{Impredicativity rules of Typer} + +%% Once we decided to try our luck with this conjecture, it was a small step to +%% add yet more potentially risky features to our calculus. So we currently +%% also allow impredicativity at all universe levels rather than only at the +%% bottom. Clearly, this risks falling victim of paradoxes like +%% Hurken's~\cite{Hurkens95}, so buyer beware: we have no yet made any serious +%% attempt at proving or disproving the soundness of this extension. + + \section{Related work} %% FIXME: re-order! View it on GitLab: https://gitlab.com/monnier/typer/commit/1347e7b4fde3f332a915af40a98438bb641… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/1347e7b4fde3f332a915af40a98438bb641… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] -
by Stefan 26 Oct '18

26 Oct '18

Stefan pushed to branch report/jfla-2019 at Stefan / Typer Commits: 45685bab by Stefan Monnier at 2018-10-26T20:04:54Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -180,10 +180,10 @@ traditional \id{map} function as follows: | nil => nil | cons x xs => cons (f x) (map f xs); \end{verbatim} -%% FIXME: It's actually not optional for recursive functions (like map). -The type declaration is optional. The triple arrow $⇛$ is used -for functions whose argument is \emph{implicit}, which is actually called -\emph{erasable} in Typer. +The type declaration is generally optional, although we currently require it +for recursive definitions. The triple arrow $⇛$ is used for functions whose +argument is \emph{implicit}, which is actually called \emph{erasable} +in Typer. %% It is the dependent function type, used to give a name to the function %% argument, so it can be used in the return type. In type theory this is %% often presented with the notation $\Pi\,x\!\:\!t_1 . t_2$, but in the above case it @@ -285,8 +285,11 @@ analysis in one step, Typer further subdivides the syntactic analysis phase into two steps. The first step does a rudimentary analysis that only extracts a generic tree structure, called S-expression. The shape of S-expressions could be described with the datatype shown in -%% FIXME: Discuss the absence of a "nil" element. -Figure~\ref{fig:Typer-Sexp}. +Figure~\ref{fig:Typer-Sexp}. Note that contrary to the Lisp S-expression +syntax, parentheses are only used for grouping purposes, so \texttt{(x)} +will produce the same \id{Sexp} as just \texttt{x}. And we use +\texttt{()} as the printed representation of the zero-length \id{symbol} +(which we call \emph{espilon}). Note how, at this stage, the representation of the code has no notion of bindings, functions, types, or function calls. It's only in a second step @@ -990,6 +993,8 @@ erasable $k$) and prove its property (again with erasable $K_1$ and $K_2$). \subsection{Impredicativity rules of Typer} +%% FIXME: Maybe remove this subsection. + Once we decided to try our luck with this conjecture, it was a small step to add yet more potentially risky features to our calculus. So we currently also allow impredicativity at all universe levels rather than only at the View it on GitLab: https://gitlab.com/monnier/typer/commit/45685bab7429afa796c08a787af0709444d… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/45685bab7429afa796c08a787af0709444d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] -
by Stefan 26 Oct '18

26 Oct '18

Stefan pushed to branch report/jfla-2019 at Stefan / Typer Commits: ccf14d4d by Stefan Monnier at 2018-10-26T18:03:30Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -8,7 +8,7 @@ \usepackage{fancyvrb} % prevent unfortunate line break in a short verbatim \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} -\DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} +\DeclareUnicodeCharacter{21DB}{\raisebox{0.15\height}{$\equiv$}\texttt{>}} \DeclareUnicodeCharacter{2980}{\ensuremath{\Vvert}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} @@ -180,6 +180,7 @@ traditional \id{map} function as follows: | nil => nil | cons x xs => cons (f x) (map f xs); \end{verbatim} +%% FIXME: It's actually not optional for recursive functions (like map). The type declaration is optional. The triple arrow $⇛$ is used for functions whose argument is \emph{implicit}, which is actually called \emph{erasable} in Typer. View it on GitLab: https://gitlab.com/monnier/typer/commit/ccf14d4ddd63730ab1dadf12cda7128f7c1… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/ccf14d4ddd63730ab1dadf12cda7128f7c1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] -
by Stefan 26 Oct '18

26 Oct '18

Stefan pushed to branch report/jfla-2019 at Stefan / Typer Commits: 1de1c2fd by Stefan Monnier at 2018-10-26T17:50:33Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -9,7 +9,7 @@ \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} \DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} -\DeclareUnicodeCharacter{2980}{\ensuremath{|||}} +\DeclareUnicodeCharacter{2980}{\ensuremath{\Vvert}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} \DeclareUnicodeCharacter{3A9}{\ensuremath{\Omega}} @@ -174,13 +174,13 @@ where \id{hd} and \id{tl} are field names. We could have written just Functions and data constructors are curried. You can define the traditional \id{map} function as follows: \begin{verbatim} - map : (a : Type) ≡> (b : Type) ≡> + map : (a : Type) ⇛ (b : Type) ⇛ (a -> b) -> List a -> List b; map f xs = case xs | nil => nil | cons x xs => cons (f x) (map f xs); \end{verbatim} -The type declaration is optional. The triple arrow $\equiv>$ is used +The type declaration is optional. The triple arrow $⇛$ is used for functions whose argument is \emph{implicit}, which is actually called \emph{erasable} in Typer. %% It is the dependent function type, used to give a name to the function @@ -228,6 +228,8 @@ They're defined simply as values with a dedicated type \id{Macro}: where \id{macro} is the constructor of the \id{Macro} type and \id{ifthen} is the function which performs the expansion. Ignoring the types, this is very similar to how it is done in Emacs Lisp. +%% FIXME: Maybe discuss the fact that we receive a *List* of Sexp rather +%% than a single Sexp as argument? The \id{ifthen} function could be defined as follows: \begin{verbatim} @@ -282,6 +284,7 @@ analysis in one step, Typer further subdivides the syntactic analysis phase into two steps. The first step does a rudimentary analysis that only extracts a generic tree structure, called S-expression. The shape of S-expressions could be described with the datatype shown in +%% FIXME: Discuss the absence of a "nil" element. Figure~\ref{fig:Typer-Sexp}. Note how, at this stage, the representation of the code has no notion of @@ -655,6 +658,10 @@ anything left to generalize); if the free meta-variable is used in a non-erasable way, we signal an error since generalizing it with an erasable abstraction would lead to invalid code. +%% FIXME: Discuss decidability/termination +%% FIXME: Is it an actual strict superset of HM (I think so, except for +%% the case of recursion where we currently require a type annotation). + There are two further places where generalization happens: when a $\lambda$ abstraction is elaborated in a context that expects an erasable function, we wrap it into an additional erasable $\lambda$; and when elaborating a \emph{type @@ -721,6 +728,7 @@ calculus are the following: } \end{array} \end{displaymath} +%% FIXME: Explain what these S/A/R mean! But the typing rule we use is slightly different for erasable functions: \begin{displaymath} \Infer{\Jtyper {\tau_1} s \\ @@ -1228,14 +1236,16 @@ making it more flexible at the same time. While it has not been officially released yet, its code can be found at \url{https://gitlab.com/monnier/typer}. +\newenvironment{acks}{\subsection*{Acknowledgments}}{} \newcommand \grantsponsor[3] {#2 (#1)} \newcommand \grantnum[2] {#2} -\subsection*{Acknowledgments} +\begin{acks} This work was supported by the \grantsponsor{NSERC}{Natural Sciences and Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} grant N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the NSERC. +\end{acks} \bibliographystyle{alpha} %% \bibliography{typer_theory} View it on GitLab: https://gitlab.com/monnier/typer/commit/1de1c2fd4861265a588d4413351ae1905fd… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/1de1c2fd4861265a588d4413351ae1905fd… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] Minor fixes, read through §5.1
by Christopher League 25 Oct '18

25 Oct '18

Christopher League pushed to branch report/jfla-2019 at Stefan / Typer Commits: c66d283d by Christopher League at 2018-10-25T20:34:32Z Minor fixes, read through §5.1 - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -5,6 +5,7 @@ \usepackage{mathpartir} \usepackage{mdframed,empheq} \usepackage{parskip} +\usepackage{fancyvrb} % prevent unfortunate line break in a short verbatim \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} \DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} @@ -101,8 +102,8 @@ support a fairly familiar infix syntax, yet simple enough that it maps straightforwardly to the equivalent of Lisp's S-expressions. While the core language lets us manipulate proofs, Typer is mostly meant to -be used as a programming language. So we wanted that the power of fully -dependent types should not unduly get in the way of programs that do not +be used as a programming language. So we wanted the power of fully +dependent types to not unduly get in the way of programs that do not make use of them. Concretely, we tried to design Typer in such a way that programs can be written with just as few extra annotations as in any other ML-family language. @@ -155,8 +156,8 @@ two core elements: functions and datatypes. To define a function which adds \end{verbatim} %% Like in Agda~\cite{Bove09}, the type of dependently typed functions is -written ``\texttt{(x :~$\tau_1$) -> $\tau_2$}''. This could also have used a bit of -a syntactic sugar to become: +written ``\texttt{(x :~$\tau_1$) -> $\tau_2$}''. The definition above +could have used a bit of a syntactic sugar to become: \begin{verbatim} add1 x = x + 1; \end{verbatim} @@ -195,20 +196,20 @@ This allows you to introduce new locally scoped definitions. The shape of this construct is ``$\texttt{let}~\id{decls}~\texttt{in}~\id{exp}$'' where \id{decls} is a sequence of declarations such as the ones shown above, separated by -semi-colons. For example, we could have defined the above map function +semicolons. For example, we could have defined the above map function as follows: -\begin{verbatim} +\begin{Verbatim}[samepage=true] map f = let map' xs = case xs | nil => nil | cons x xs => cons (f x) (map' xs) in map' -\end{verbatim} -%As you can guess from this example, +\end{Verbatim} +%As you can guess from this example, Typer has fundamentally two syntactic categories: expressions and declarations. A Typer file is defined as a sequence of declarations, -separated by semi-colons. +separated by semicolons. %% Most Lisps manage to conflate those two %% categories, but in our case, we were unable to unify them without %% introducing more problems. E.g. Common-Lisp solves the problem by treating @@ -253,7 +254,7 @@ Wherever the above macro is in scope, the programmer can write: Being purely functional, Typer resorts to the usual monadic technique to get access to a side effecting world, just as is done in Haskell. In the above code, \id{ME} is the macro-expansion monad, used for the same purpose as the -one used in Template Haskell~\cite{Sheard02}, and \id{return} is the unit of +one in Template Haskell~\cite{Sheard02}, and \id{return} is the unit of that monad. \section{Syntactic structure} View it on GitLab: https://gitlab.com/monnier/typer/commit/c66d283dc66754364efd4851b25e08a8e16… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/c66d283dc66754364efd4851b25e08a8e16… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/jfla-2019] -
by Stefan 25 Oct '18

25 Oct '18

Stefan pushed to branch report/jfla-2019 at Stefan / Typer Commits: 17a8e0c1 by Stefan Monnier at 2018-10-25T15:53:50Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -995,6 +995,8 @@ discussed by Fruchart and Longo in~\cite{Fruchart96}. \section{Related work} +%% FIXME: re-order! + %% FIXME: Shorten, and then add things: %% F-star? ATS? @@ -1227,8 +1229,7 @@ While it has not been officially released yet, its code can be found at \newcommand \grantsponsor[3] {#2 (#1)} \newcommand \grantnum[2] {#2} - -\section*{Acknowledgments} +\subsection*{Acknowledgments} This work was supported by the \grantsponsor{NSERC}{Natural Sciences and Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} grant N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and View it on GitLab: https://gitlab.com/monnier/typer/commit/17a8e0c144781e4fe5ddd76fdef03a01ed1… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/17a8e0c144781e4fe5ddd76fdef03a01ed1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/itd] -
by Stefan 25 Oct '18

25 Oct '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: dfd1bc56 by Stefan Monnier at 2018-10-25T15:06:06Z - - - - - - 3 changed files: - + llncs.cls - + llncs2e/llncs.cls - paper.tex Changes: ===================================== llncs.cls ===================================== @@ -0,0 +1 @@ +llncs2e/llncs.cls \ No newline at end of file ===================================== llncs2e/llncs.cls ===================================== @@ -0,0 +1,1218 @@ +% LLNCS DOCUMENT CLASS -- version 2.20 (10-Mar-2018) +% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science +% +%% +%% \CharacterTable +%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +%% Digits \0\1\2\3\4\5\6\7\8\9 +%% Exclamation \! Double quote \" Hash (number) \# +%% Dollar \$ Percent \% Ampersand \& +%% Acute accent \' Left paren $ Right paren $ +%% Asterisk \* Plus \+ Comma \, +%% Minus \- Point \. Solidus \/ +%% Colon \: Semicolon \; Less than \< +%% Equals \= Greater than \> Question mark \? +%% Commercial at \@ Left bracket \[ Backslash \\ +%% Right bracket \] Circumflex \^ Underscore \_ +%% Grave accent \` Left brace \{ Vertical bar \| +%% Right brace \} Tilde \~} +%% +\NeedsTeXFormat{LaTeX2e}[1995/12/01] +\ProvidesClass{llncs}[2018/03/10 v2.20 +^^J LaTeX document class for Lecture Notes in Computer Science] +% Options +\let\if@envcntreset\iffalse +\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue} +\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y} +\DeclareOption{oribibl}{\let\oribibl=Y} +\let\if@custvec\iftrue +\DeclareOption{orivec}{\let\if@custvec\iffalse} +\let\if@envcntsame\iffalse +\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue} +\let\if@envcntsect\iffalse +\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue} +\let\if@runhead\iffalse +\DeclareOption{runningheads}{\let\if@runhead\iftrue} + +\let\if@openright\iftrue +\let\if@openbib\iffalse +\DeclareOption{openbib}{\let\if@openbib\iftrue} + +% languages +\let\switcht@@therlang\relax +\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}} +\def\ds@francais{\def\switcht@@therlang{\switcht@francais}} + +\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} + +\ProcessOptions + +\LoadClass[twoside]{article} +\RequirePackage{multicol} % needed for the list of participants, index +\RequirePackage{aliascnt} + +\setlength{\textwidth}{12.2cm} +\setlength{\textheight}{19.3cm} +\renewcommand\@pnumwidth{2em} +\renewcommand\(a)tocrmarg{3.5em} +% +\def\@dottedtocline#1#2#3#4#5{% + \ifnum #1>\c@tocdepth \else + \vskip \z@ \@plus.2\p@ + {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm + \parfillskip -\rightskip \pretolerance=10000 + \parindent #2\relax\@afterindenttrue + \interlinepenalty\@M + \leavevmode + \@tempdima #3\relax + \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip + {#4}\nobreak + \leaders\hbox{$\m@th + \mkern \@dotsep mu\hbox{.}\mkern \@dotsep + mu$}\hfill + \nobreak + \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}% + \par}% + \fi} +% +\def\switcht@albion{% +\def\abstractname{Abstract.} +\def\ackname{Acknowledgement.} +\def\andname{and} +\def\lastandname{\unskip, and} +\def\appendixname{Appendix} +\def\chaptername{Chapter} +\def\claimname{Claim} +\def\conjecturename{Conjecture} +\def\contentsname{Table of Contents} +\def\corollaryname{Corollary} +\def\definitionname{Definition} +\def\examplename{Example} +\def\exercisename{Exercise} +\def\figurename{Fig.} +\def\keywordname{{\bf Keywords:}} +\def\indexname{Index} +\def\lemmaname{Lemma} +\def\contriblistname{List of Contributors} +\def\listfigurename{List of Figures} +\def\listtablename{List of Tables} +\def\mailname{{\it Correspondence to\/}:} +\def\noteaddname{Note added in proof} +\def\notename{Note} +\def\partname{Part} +\def\problemname{Problem} +\def\proofname{Proof} +\def\propertyname{Property} +\def\propositionname{Proposition} +\def\questionname{Question} +\def\remarkname{Remark} +\def\seename{see} +\def\solutionname{Solution} +\def\subclassname{{\it Subject Classifications\/}:} +\def\tablename{Table} +\def\theoremname{Theorem}} +\switcht@albion +% Names of theorem like environments are already defined +% but must be translated if another language is chosen +% +% French section +\def\switcht@francais{%\typeout{On parle francais.}% + \def\abstractname{R\'esum\'e.}% + \def\ackname{Remerciements.}% + \def\andname{et}% + \def\lastandname{ et}% + \def\appendixname{Appendice} + \def\chaptername{Chapitre}% + \def\claimname{Pr\'etention}% + \def\conjecturename{Hypoth\`ese}% + \def\contentsname{Table des mati\`eres}% + \def\corollaryname{Corollaire}% + \def\definitionname{D\'efinition}% + \def\examplename{Exemple}% + \def\exercisename{Exercice}% + \def\figurename{Fig.}% + \def\keywordname{{\bf Mots-cl\'e:}} + \def\indexname{Index} + \def\lemmaname{Lemme}% + \def\contriblistname{Liste des contributeurs} + \def\listfigurename{Liste des figures}% + \def\listtablename{Liste des tables}% + \def\mailname{{\it Correspondence to\/}:} + \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}% + \def\notename{Remarque}% + \def\partname{Partie}% + \def\problemname{Probl\`eme}% + \def\proofname{Preuve}% + \def\propertyname{Caract\'eristique}% +%\def\propositionname{Proposition}% + \def\questionname{Question}% + \def\remarkname{Remarque}% + \def\seename{voir} + \def\solutionname{Solution}% + \def\subclassname{{\it Subject Classifications\/}:} + \def\tablename{Tableau}% + \def\theoremname{Th\'eor\`eme}% +} +% +% German section +\def\switcht@deutsch{%\typeout{Man spricht deutsch.}% + \def\abstractname{Zusammenfassung.}% + \def\ackname{Danksagung.}% + \def\andname{und}% + \def\lastandname{ und}% + \def\appendixname{Anhang}% + \def\chaptername{Kapitel}% + \def\claimname{Behauptung}% + \def\conjecturename{Hypothese}% + \def\contentsname{Inhaltsverzeichnis}% + \def\corollaryname{Korollar}% +%\def\definitionname{Definition}% + \def\examplename{Beispiel}% + \def\exercisename{\"Ubung}% + \def\figurename{Abb.}% + \def\keywordname{{\bf Schl\"usselw\"orter:}} + \def\indexname{Index} +%\def\lemmaname{Lemma}% + \def\contriblistname{Mitarbeiter} + \def\listfigurename{Abbildungsverzeichnis}% + \def\listtablename{Tabellenverzeichnis}% + \def\mailname{{\it Correspondence to\/}:} + \def\noteaddname{Nachtrag}% + \def\notename{Anmerkung}% + \def\partname{Teil}% +%\def\problemname{Problem}% + \def\proofname{Beweis}% + \def\propertyname{Eigenschaft}% +%\def\propositionname{Proposition}% + \def\questionname{Frage}% + \def\remarkname{Anmerkung}% + \def\seename{siehe} + \def\solutionname{L\"osung}% + \def\subclassname{{\it Subject Classifications\/}:} + \def\tablename{Tabelle}% +%\def\theoremname{Theorem}% +} + +% Ragged bottom for the actual page +\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil +\global\let\@textbottom\relax}} + +\renewcommand\small{% + \@setfontsize\small\@ixpt{11}% + \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus2\p@ + \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \parsep 0\p@ \@plus1\p@ \@minus\p@ + \topsep 8\p@ \@plus2\p@ \@minus4\p@ + \itemsep0\p@}% + \belowdisplayskip \abovedisplayskip +} + +\frenchspacing +\widowpenalty=10000 +\clubpenalty=10000 + +\setlength\oddsidemargin {63\p@} +\setlength\evensidemargin {63\p@} +\setlength\marginparwidth {90\p@} + +\setlength\headsep {16\p@} + +\setlength\footnotesep{7.7\p@} +\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@} +\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@} + +\setcounter{secnumdepth}{2} + +\newcounter {chapter} +\renewcommand\thechapter {\@arabic\c@chapter} + +\newif\if@mainmatter \@mainmattertrue +\newcommand\frontmatter{\cleardoublepage + \@mainmatterfalse\pagenumbering{Roman}} +\newcommand\mainmatter{\cleardoublepage + \@mainmattertrue\pagenumbering{arabic}} +\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi + \@mainmatterfalse} + +\renewcommand\part{\cleardoublepage + \thispagestyle{empty}% + \if@twocolumn + \onecolumn + \@tempswatrue + \else + \@tempswafalse + \fi + \null\vfil + \secdef\@part\@spart} + +\def\@part[#1]#2{% + \ifnum \c@secnumdepth >-2\relax + \refstepcounter{part}% + \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}% + \else + \addcontentsline{toc}{part}{#1}% + \fi + \markboth{}{}% + {\centering + \interlinepenalty \@M + \normalfont + \ifnum \c@secnumdepth >-2\relax + \huge\bfseries \partname~\thepart + \par + \vskip 20\p@ + \fi + \Huge \bfseries #2\par}% + \@endpart} +\def\@spart#1{% + {\centering + \interlinepenalty \@M + \normalfont + \Huge \bfseries #1\par}% + \@endpart} +\def\@endpart{\vfil\newpage + \if@twoside + \null + \thispagestyle{empty}% + \newpage + \fi + \if@tempswa + \twocolumn + \fi} + +\newcommand\chapter{\clearpage + \thispagestyle{empty}% + \global\@topnum\z@ + \@afterindentfalse + \secdef\@chapter\@schapter} +\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne + \if@mainmatter + \refstepcounter{chapter}% + \typeout{\(a)chapapp\space\thechapter.}% + \addcontentsline{toc}{chapter}% + {\protect\numberline{\thechapter}#1}% + \else + \addcontentsline{toc}{chapter}{#1}% + \fi + \else + \addcontentsline{toc}{chapter}{#1}% + \fi + \chaptermark{#1}% + \addtocontents{lof}{\protect\addvspace{10\p@}}% + \addtocontents{lot}{\protect\addvspace{10\p@}}% + \if@twocolumn + \@topnewpage[\@makechapterhead{#2}]% + \else + \@makechapterhead{#2}% + \@afterheading + \fi} +\def\@makechapterhead#1{% +% \vspace*{50\p@}% + {\centering + \ifnum \c@secnumdepth >\m@ne + \if@mainmatter + \large\bfseries \@chapapp{} \thechapter + \par\nobreak + \vskip 20\p@ + \fi + \fi + \interlinepenalty\@M + \Large \bfseries #1\par\nobreak + \vskip 40\p@ + }} +\def\@schapter#1{\if@twocolumn + \@topnewpage[\@makeschapterhead{#1}]% + \else + \@makeschapterhead{#1}% + \@afterheading + \fi} +\def\@makeschapterhead#1{% +% \vspace*{50\p@}% + {\centering + \normalfont + \interlinepenalty\@M + \Large \bfseries #1\par\nobreak + \vskip 40\p@ + }} + +\renewcommand\section{\@startsection{section}{1}{\z@}% + {-18\p@ \@plus -4\p@ \@minus -4\p@}% + {12\p@ \@plus 4\p@ \@minus 4\p@}% + {\normalfont\large\bfseries\boldmath + \rightskip=\z@ \@plus 8em\pretolerance=10000 }} +\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% + {-18\p@ \@plus -4\p@ \@minus -4\p@}% + {8\p@ \@plus 4\p@ \@minus 4\p@}% + {\normalfont\normalsize\bfseries\boldmath + \rightskip=\z@ \@plus 8em\pretolerance=10000 }} +\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% + {-18\p@ \@plus -4\p@ \@minus -4\p@}% + {-0.5em \@plus -0.22em \@minus -0.1em}% + {\normalfont\normalsize\bfseries\boldmath}} +\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% + {-12\p@ \@plus -4\p@ \@minus -4\p@}% + {-0.5em \@plus -0.22em \@minus -0.1em}% + {\normalfont\normalsize\itshape}} +\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use + \string\subparagraph\space with this class}\vskip0.5cm +You should not use \verb|\subparagraph| with this class.\vskip0.5cm} + +\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00} +\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01} +\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02} +\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03} +\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04} +\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05} +\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06} +\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07} +\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08} +\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09} +\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A} + +\let\footnotesize\small + +\if@custvec +\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}} +{\mbox{\boldmath$\textstyle#1$}} +{\mbox{\boldmath$\scriptstyle#1$}} +{\mbox{\boldmath$\scriptscriptstyle#1$}}} +\fi + +\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}} +\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil +\penalty50\hskip1em\null\nobreak\hfil\squareforqed +\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi} + +\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip +\halign{\hfil +$\displaystyle##$\hfil\cr\gets\cr\to\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets +\cr\to\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets +\cr\to\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +\gets\cr\to\cr}}}}} +\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil +$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr +\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr +\noalign{\vskip1pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +<\cr +\noalign{\vskip0.9pt}=\cr}}}}} +\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil +$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr +\noalign{\vskip1.2pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr +\noalign{\vskip1pt}=\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +>\cr +\noalign{\vskip0.9pt}=\cr}}}}} +\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip +\halign{\hfil +$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr +>\cr\noalign{\vskip-1pt}<\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr +>\cr\noalign{\vskip-0.8pt}<\cr}}} +{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr +>\cr\noalign{\vskip-0.3pt}<\cr}}}}} +\def\bbbr{{\rm I\!R}} %reelle Zahlen +\def\bbbm{{\rm I\!M}} +\def\bbbn{{\rm I\!N}} %natuerliche Zahlen +\def\bbbf{{\rm I\!F}} +\def\bbbh{{\rm I\!H}} +\def\bbbk{{\rm I\!K}} +\def\bbbp{{\rm I\!P}} +\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l} +{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}} +\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox +to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}} +\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm +Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise +0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}} +\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm +T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox +to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox +to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox +to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}} +\def\bbbs{{\mathchoice +{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox +to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} +{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox +to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox +to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}} +{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox +to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox +to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}} +\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} +{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}} +{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}} +{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}} + +\let\ts\, + +\setlength\leftmargini {17\p@} +\setlength\leftmargin {\leftmargini} +\setlength\leftmarginii {\leftmargini} +\setlength\leftmarginiii {\leftmargini} +\setlength\leftmarginiv {\leftmargini} +\setlength \labelsep {.5em} +\setlength \labelwidth{\leftmargini} +\addtolength\labelwidth{-\labelsep} + +\def\@listI{\leftmargin\leftmargini + \parsep 0\p@ \@plus1\p@ \@minus\p@ + \topsep 8\p@ \@plus2\p@ \@minus4\p@ + \itemsep0\p@} +\let\@listi\@listI +\@listi +\def\@listii {\leftmargin\leftmarginii + \labelwidth\leftmarginii + \advance\labelwidth-\labelsep + \topsep 0\p@ \@plus2\p@ \@minus\p@} +\def\@listiii{\leftmargin\leftmarginiii + \labelwidth\leftmarginiii + \advance\labelwidth-\labelsep + \topsep 0\p@ \@plus\p@\@minus\p@ + \parsep \z@ + \partopsep \p@ \@plus\z@ \@minus\p@} + +\renewcommand\labelitemi{\normalfont\bfseries --} +\renewcommand\labelitemii{$\m@th\bullet$} + +\setlength\arraycolsep{1.4\p@} +\setlength\tabcolsep{1.4\p@} + +\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}% + {{\contentsname}}} + \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}} + \def\lastand{\ifnum\value{auco}=2\relax + \unskip{} \andname\ + \else + \unskip \lastandname\ + \fi}% + \def\and{\stepcounter{@auth}\relax + \ifnum\value{@auth}=\value{auco}% + \lastand + \else + \unskip, + \fi}% + \@starttoc{toc}\if@restonecol\twocolumn\fi} + +\def\l@part#1#2{\addpenalty{\@secpenalty}% + \addvspace{2em plus\p@}% % space above part line + \begingroup + \parindent \z@ + \rightskip \z@ plus 5em + \hrule\vskip5pt + \large % same size as for a contribution heading + \bfseries\boldmath % set line in boldface + \leavevmode % TeX command to enter horizontal mode. + #1\par + \vskip5pt + \hrule + \vskip1pt + \nobreak % Never break after part entry + \endgroup} + +\def\@dotsep{2} + +\let\phantomsection=\relax + +\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else +{}\fi} + +\def\addnumcontentsmark#1#2#3{% +\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline + {\thechapter}#3}{\thepage}\hyperhrefextend}}% +\def\addcontentsmark#1#2#3{% +\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}% +\def\addcontentsmarkwop#1#2#3{% +\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}% + +\def\@adcmk[#1]{\ifcase #1 \or +\def\@gtempa{\addnumcontentsmark}% + \or \def\@gtempa{\addcontentsmark}% + \or \def\@gtempa{\addcontentsmarkwop}% + \fi\@gtempa{toc}{chapter}% +} +\def\addtocmark{% +\phantomsection +\@ifnextchar[{\@adcmk}{\@adcmk[3]}% +} + +\def\l@chapter#1#2{\addpenalty{-\@highpenalty} + \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup + \parindent \z@ \rightskip \@tocrmarg + \advance\rightskip by 0pt plus 2cm + \parfillskip -\rightskip \pretolerance=10000 + \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip + {\large\bfseries\boldmath#1}\ifx0#2\hfil\null + \else + \nobreak + \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern + \@dotsep mu$}\hfill + \nobreak\hbox to\@pnumwidth{\hss #2}% + \fi\par + \penalty\@highpenalty \endgroup} + +\def\l@title#1#2{\addpenalty{-\@highpenalty} + \addvspace{8pt plus 1pt} + \@tempdima \z@ + \begingroup + \parindent \z@ \rightskip \@tocrmarg + \advance\rightskip by 0pt plus 2cm + \parfillskip -\rightskip \pretolerance=10000 + \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip + #1\nobreak + \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern + \@dotsep mu$}\hfill + \nobreak\hbox to\@pnumwidth{\hss #2}\par + \penalty\@highpenalty \endgroup} + +\def\l@author#1#2{\addpenalty{\@highpenalty} + \@tempdima=15\p@ %\z@ + \begingroup + \parindent \z@ \rightskip \@tocrmarg + \advance\rightskip by 0pt plus 2cm + \pretolerance=10000 + \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip + \textit{#1}\par + \penalty\@highpenalty \endgroup} + +\setcounter{tocdepth}{0} +\newdimen\tocchpnum +\newdimen\tocsecnum +\newdimen\tocsectotal +\newdimen\tocsubsecnum +\newdimen\tocsubsectotal +\newdimen\tocsubsubsecnum +\newdimen\tocsubsubsectotal +\newdimen\tocparanum +\newdimen\tocparatotal +\newdimen\tocsubparanum +\tocchpnum=\z@ % no chapter numbers +\tocsecnum=15\p@ % section 88. plus 2.222pt +\tocsubsecnum=23\p@ % subsection 88.8 plus 2.222pt +\tocsubsubsecnum=27\p@ % subsubsection 88.8.8 plus 1.444pt +\tocparanum=35\p@ % paragraph 88.8.8.8 plus 1.666pt +\tocsubparanum=43\p@ % subparagraph 88.8.8.8.8 plus 1.888pt +\def\calctocindent{% +\tocsectotal=\tocchpnum +\advance\tocsectotal by\tocsecnum +\tocsubsectotal=\tocsectotal +\advance\tocsubsectotal by\tocsubsecnum +\tocsubsubsectotal=\tocsubsectotal +\advance\tocsubsubsectotal by\tocsubsubsecnum +\tocparatotal=\tocsubsubsectotal +\advance\tocparatotal by\tocparanum} +\calctocindent + +\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}} +\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}} +\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}} +\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}} +\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}} + +\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn + \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}} + \@starttoc{lof}\if@restonecol\twocolumn\fi} +\def\l@figure{\@dottedtocline{1}{0em}{1.5em}} + +\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn + \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}} + \@starttoc{lot}\if@restonecol\twocolumn\fi} +\let\l@table\l@figure + +\renewcommand\listoffigures{% + \section*{\listfigurename + \@mkboth{\listfigurename}{\listfigurename}}% + \@starttoc{lof}% + } + +\renewcommand\listoftables{% + \section*{\listtablename + \@mkboth{\listtablename}{\listtablename}}% + \@starttoc{lot}% + } + +\ifx\oribibl\undefined +\ifx\citeauthoryear\undefined +\renewenvironment{thebibliography}[1] + {\section*{\refname} + \def\(a)biblabel##1{##1.} + \small + \list{\@biblabel{\@arabic\c@enumiv}}% + {\settowidth\labelwidth{\@biblabel{#1}}% + \leftmargin\labelwidth + \advance\leftmargin\labelsep + \if@openbib + \advance\leftmargin\bibindent + \itemindent -\bibindent + \listparindent \itemindent + \parsep \z@ + \fi + \usecounter{enumiv}% + \let\p@enumiv\@empty + \renewcommand\theenumiv{\@arabic\c@enumiv}}% + \if@openbib + \renewcommand\newblock{\par}% + \else + \renewcommand\newblock{\hskip .11em \(a)plus.33em \(a)minus.07em}% + \fi + \sloppy\clubpenalty4000\widowpenalty4000% + \sfcode`\.=\@m} + {\def\@noitemerr + {\@latex@warning{Empty `thebibliography' environment}}% + \endlist} +\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw + {\let\protect\noexpand\immediate + \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} +\newcount\@tempcntc +\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi + \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do + {\@ifundefined + {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries + ?}\@warning + {Citation `\@citeb' on page \thepage \space undefined}}% + {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}% + \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne + \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}% + \else + \advance\@tempcntb\@ne + \ifnum\@tempcntb=\@tempcntc + \else\advance\@tempcntb\m@ne\@citeo + \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}} +\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else + \@citea\def\@citea{,\,\hskip\z@skip}% + \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else + {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else + \def\@citea{--}\fi + \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi} +\else +\renewenvironment{thebibliography}[1] + {\section*{\refname} + \small + \list{}% + {\settowidth\labelwidth{}% + \leftmargin\parindent + \itemindent=-\parindent + \labelsep=\z@ + \if@openbib + \advance\leftmargin\bibindent + \itemindent -\bibindent + \listparindent \itemindent + \parsep \z@ + \fi + \usecounter{enumiv}% + \let\p@enumiv\@empty + \renewcommand\theenumiv{}}% + \if@openbib + \renewcommand\newblock{\par}% + \else + \renewcommand\newblock{\hskip .11em \(a)plus.33em \(a)minus.07em}% + \fi + \sloppy\clubpenalty4000\widowpenalty4000% + \sfcode`\.=\@m} + {\def\@noitemerr + {\@latex@warning{Empty `thebibliography' environment}}% + \endlist} + \def\@cite#1{#1}% + \def\@lbibitem[#1]#2{\item[]\if@filesw + {\def\protect##1{\string ##1\space}\immediate + \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces} + \fi +\else +\@cons\@openbib@code{\noexpand\small} +\fi + +\def\idxquad{\hskip 10\p@}% space that divides entry from number + +\def\@idxitem{\par\hangindent 10\p@} + +\def\subitem{\par\setbox0=\hbox{--\enspace}% second order + \noindent\hangindent\wd0\box0}% index entry + +\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third + \noindent\hangindent\wd0\box0}% order index entry + +\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax} + +\renewenvironment{theindex} + {\@mkboth{\indexname}{\indexname}% + \thispagestyle{empty}\parindent\z@ + \parskip\z@ \@plus .3\p@\relax + \let\item\par + \def\,{\relax\ifmmode\mskip\thinmuskip + \else\hskip0.2em\ignorespaces\fi}% + \normalfont\small + \begin{multicols}{2}[\@makeschapterhead{\indexname}]% + } + {\end{multicols}} + +\renewcommand\footnoterule{% + \kern-3\p@ + \hrule\@width 2truecm + \kern2.6\p@} + \newdimen\fnindent + \fnindent1em +\long\def\@makefntext#1{% + \parindent \fnindent% + \leftskip \fnindent% + \noindent + \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1} + +\long\def\@makecaption#1#2{% + \small + \vskip\abovecaptionskip + \sbox\@tempboxa{{\bfseries #1.} #2}% + \ifdim \wd\@tempboxa >\hsize + {\bfseries #1.} #2\par + \else + \global \@minipagefalse + \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}% + \fi + \vskip\belowcaptionskip} + +\def\fps@figure{htbp} +\def\fnum@figure{\figurename\thinspace\thefigure} +\def \@floatboxreset {% + \reset@font + \small + \@setnobreak + \@setminipage +} +\def\fps@table{htbp} +\def\fnum@table{\tablename~\thetable} +\renewenvironment{table} + {\setlength\abovecaptionskip{0\p@}% + \setlength\belowcaptionskip{10\p@}% + \@float{table}} + {\end@float} +\renewenvironment{table*} + {\setlength\abovecaptionskip{0\p@}% + \setlength\belowcaptionskip{10\p@}% + \@dblfloat{table}} + {\end@dblfloat} + +\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname + ext@#1\endcsname}{#1}{\protect\numberline{\csname + the#1\endcsname}{\ignorespaces #2}}\begingroup + \@parboxrestore + \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par + \endgroup} + +% LaTeX does not provide a command to enter the authors institute +% addresses. The \institute command is defined here. + +\newcounter{@inst} +\newcounter{@auth} +\newcounter{auco} +\newdimen\instindent +\newbox\authrun +\newtoks\authorrunning +\newtoks\tocauthor +\newbox\titrun +\newtoks\titlerunning +\newtoks\toctitle + +\def\clearheadinfo{\gdef\@author{No Author Given}% + \gdef\@title{No Title Given}% + \gdef\@subtitle{}% + \gdef\@institute{No Institute Given}% + \gdef\@thanks{}% + \global\titlerunning={}\global\authorrunning={}% + \global\toctitle={}\global\tocauthor={}} + +\def\institute#1{\gdef\@institute{#1}} + +\def\institutename{\par + \begingroup + \parskip=\z@ + \parindent=\z@ + \setcounter{@inst}{1}% + \def\and{\par\stepcounter{@inst}% + \noindent$^{\the@inst}$\enspace\ignorespaces}% + \setbox0=\vbox{\def\thanks##1{}\@institute}% + \ifnum\c@@inst=1\relax + \gdef\fnnstart{0}% + \else + \xdef\fnnstart{\c@@inst}% + \setcounter{@inst}{1}% + \noindent$^{\the@inst}$\enspace + \fi + \ignorespaces + \@institute\par + \endgroup} + +\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or + {\star\star\star}\or \dagger\or \ddagger\or + \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger + \or \ddagger\ddagger \else\@ctrerr\fi}} + +\def\inst#1{\unskip$^{#1}$} +\def\orcidID#1{\unskip$^{[#1]}$} % added MR 2018-03-10 +\def\fnmsep{\unskip$^,$} +\def\email#1{{\tt#1}} + +\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}% +\@ifpackageloaded{babel}{% +\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}% +\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}% +\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}% +\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}% +}{\switcht@@therlang}% +\providecommand{\keywords}[1]{\def\and{{\textperiodcentered} }% +\par\addvspace\baselineskip +\noindent\keywordname\enspace\ignorespaces#1}% +\@ifpackageloaded{hyperref}{% +\def\doi#1{\href{https://doi.org/#1}{https://doi.org/#1}}}{ +\def\doi#1{https://doi.org/#1}} +} +\def\homedir{\~{ }} + +\def\subtitle#1{\gdef\@subtitle{#1}} +\clearheadinfo +% +%%% to avoid hyperref warnings +\providecommand*{\toclevel@author}{999} +%%% to make title-entry parent of section-entries +\providecommand*{\toclevel@title}{0} +% +\renewcommand\maketitle{\newpage +\phantomsection + \refstepcounter{chapter}% + \stepcounter{section}% + \setcounter{section}{0}% + \setcounter{subsection}{0}% + \setcounter{figure}{0} + \setcounter{table}{0} + \setcounter{equation}{0} + \setcounter{footnote}{0}% + \begingroup + \parindent=\z@ + \renewcommand\thefootnote{\@fnsymbol\c@footnote}% + \if@twocolumn + \ifnum \col@number=\@ne + \@maketitle + \else + \twocolumn[\@maketitle]% + \fi + \else + \newpage + \global\@topnum\z@ % Prevents figures from going at top of page. + \@maketitle + \fi + \thispagestyle{empty}\@thanks +% + \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}% + \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}% + \instindent=\hsize + \advance\instindent by-\headlineindent + \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else + \addcontentsline{toc}{title}{\the\toctitle}\fi + \if@runhead + \if!\the\titlerunning!\else + \edef\@title{\the\titlerunning}% + \fi + \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}% + \ifdim\wd\titrun>\instindent + \typeout{Title too long for running head. Please supply}% + \typeout{a shorter form with \string\titlerunning\space prior to + \string\maketitle}% + \global\setbox\titrun=\hbox{\small\rm + Title Suppressed Due to Excessive Length}% + \fi + \xdef\@title{\copy\titrun}% + \fi +% + \if!\the\tocauthor!\relax + {\def\and{\noexpand\protect\noexpand\and}% + \def\inst##1{}% added MR 2017-09-20 to remove inst numbers from the TOC + \def\orcidID##1{}% added MR 2017-09-20 to remove ORCID ids from the TOC + \protected@xdef\toc@uthor{\@author}}% + \else + \def\\{\noexpand\protect\noexpand\newline}% + \protected@xdef\scratch{\the\tocauthor}% + \protected@xdef\toc@uthor{\scratch}% + \fi + \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}% + \addcontentsline{toc}{author}{\toc@uthor}% + \if@runhead + \if!\the\authorrunning! + \value{@inst}=\value{@auth}% + \setcounter{@auth}{1}% + \else + \edef\@author{\the\authorrunning}% + \fi + \global\setbox\authrun=\hbox{\def\inst##1{}% added MR 2017-09-20 to remove inst numbers from the runninghead + \def\orcidID##1{}% added MR 2017-09-20 to remove ORCID ids from the runninghead + \small\unboldmath\@author\unskip}% + \ifdim\wd\authrun>\instindent + \typeout{Names of authors too long for running head. Please supply}% + \typeout{a shorter form with \string\authorrunning\space prior to + \string\maketitle}% + \global\setbox\authrun=\hbox{\small\rm + Authors Suppressed Due to Excessive Length}% + \fi + \xdef\@author{\copy\authrun}% + \markboth{\@author}{\@title}% + \fi + \endgroup + \setcounter{footnote}{\fnnstart}% + \clearheadinfo} +% +\def\@maketitle{\newpage + \markboth{}{}% + \def\lastand{\ifnum\value{@inst}=2\relax + \unskip{} \andname\ + \else + \unskip \lastandname\ + \fi}% + \def\and{\stepcounter{@auth}\relax + \ifnum\value{@auth}=\value{@inst}% + \lastand + \else + \unskip, + \fi}% + \begin{center}% + \let\newline\\ + {\Large \bfseries\boldmath + \pretolerance=10000 + \@title \par}\vskip .8cm +\if!\@subtitle!\else {\large \bfseries\boldmath + \vskip -.65cm + \pretolerance=10000 + \@subtitle \par}\vskip .8cm\fi + \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}% + \def\thanks##1{}\@author}% + \global\value{@inst}=\value{@auth}% + \global\value{auco}=\value{@auth}% + \setcounter{@auth}{1}% +{\lineskip .5em +\noindent\ignorespaces +\(a)author\vskip.35cm} + {\small\institutename} + \end{center}% + } + +% definition of the "\spnewtheorem" command. +% +% Usage: +% +% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font} +% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font} +% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font} +% +% New is "cap_font" and "body_font". It stands for +% fontdefinition of the caption and the text itself. +% +% "\spnewtheorem*" gives a theorem without number. +% +% A defined spnewthoerem environment is used as described +% by Lamport. +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\@thmcountersep{} +\def\(a)thmcounterend{.} + +\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}} + +% definition of \spnewtheorem with number + +\def\@spnthm#1#2{% + \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}} +\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}} + +\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}\@addtoreset{#1}{#3}% + \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand + \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname + {\@definecounter{#1}% + \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@spothm#1[#2]#3#4#5{% + \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}% + {\expandafter\@ifdefinable\csname #1\endcsname + {\newaliascnt{#1}{#2}% + \expandafter\xdef\csname #1name\endcsname{#3}% + \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}% + \global\@namedef{end#1}{\@endtheorem}}}} + +\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@ +\refstepcounter{#1}% +\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}} + +\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}% + \ignorespaces} + +\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname + the#1\endcsname}{#5}{#3}{#4}\ignorespaces} + +\def\@spbegintheorem#1#2#3#4{\trivlist + \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4} + +\def\@spopargbegintheorem#1#2#3#4#5{\trivlist + \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5} + +% definition of \spnewtheorem* without number + +\def\@sthm#1#2{\@Ynthm{#1}{#2}} + +\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname + {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}% + \expandafter\xdef\csname #1name\endcsname{#2}% + \global\@namedef{end#1}{\@endtheorem}}} + +\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@ +\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}} + +\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces} + +\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1} + {#4}{#2}{#3}\ignorespaces} + +\def\@Begintheorem#1#2#3{#3\trivlist + \item[\hskip\labelsep{#2#1\@thmcounterend}]} + +\def\@Opargbegintheorem#1#2#3#4{#4\trivlist + \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }} + +\if@envcntsect + \def\(a)thmcountersep{.} + \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape} +\else + \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape} + \if@envcntreset + \@addtoreset{theorem}{section} + \else + \@addtoreset{theorem}{chapter} + \fi +\fi + +%definition of divers theorem environments +\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily} +\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily} +\if@envcntsame % alle Umgebungen wie Theorem. + \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}} +\else % alle Umgebungen mit eigenem Zaehler + \if@envcntsect % mit section numeriert + \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}} + \else % nicht mit section numeriert + \if@envcntreset + \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} + \@addtoreset{#1}{section}} + \else + \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4} + \@addtoreset{#1}{chapter}}% + \fi + \fi +\fi +\spn@wtheorem{case}{Case}{\itshape}{\rmfamily} +\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily} +\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape} +\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape} +\spn@wtheorem{example}{Example}{\itshape}{\rmfamily} +\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily} +\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape} +\spn@wtheorem{note}{Note}{\itshape}{\rmfamily} +\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily} +\spn@wtheorem{property}{Property}{\itshape}{\rmfamily} +\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape} +\spn@wtheorem{question}{Question}{\itshape}{\rmfamily} +\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily} +\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily} + +\def\@takefromreset#1#2{% + \def\@tempa{#1}% + \let\@tempd\@elt + \def\@elt##1{% + \def\@tempb{##1}% + \ifx\@tempa\@tempb\else + \@addtoreset{##1}{#2}% + \fi}% + \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname + \expandafter\def\csname cl@#2\endcsname{}% + \@tempc + \let\@elt\@tempd} + +\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist + \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5} + \def\@Opargbegintheorem##1##2##3##4{##4\trivlist + \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }} + } + +\renewenvironment{abstract}{% + \list{}{\advance\topsep by0.35cm\relax\small + \leftmargin=1cm + \labelwidth=\z@ + \listparindent=\z@ + \itemindent\listparindent + \rightmargin\leftmargin}\item[\hskip\labelsep + \bfseries\abstractname]} + {\endlist} + +\newdimen\headlineindent % dimension for space between +\headlineindent=1.166cm % number and text of headings. + +\def\ps@headings{\let\@mkboth\@gobbletwo + \let\@oddfoot\@empty\let\@evenfoot\@empty + \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% + \leftmark\hfil} + \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}% + \llap{\thepage}} + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} + +\def\ps@titlepage{\let\@mkboth\@gobbletwo + \let\@oddfoot\@empty\let\@evenfoot\@empty + \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}% + \hfil} + \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}% + \llap{\thepage}} + \def\chaptermark##1{}% + \def\sectionmark##1{}% + \def\subsectionmark##1{}} + +\if@runhead\ps@headings\else +\ps@empty\fi + +\setlength\arraycolsep{1.4\p@} +\setlength\tabcolsep{1.4\p@} + +\endinput +%end of file llncs.cls ===================================== paper.tex ===================================== @@ -1,5 +1,5 @@ -\documentclass[sigplan,10pt,review]{acmart} -\settopmatter{printfolios=true,printccs=false,printacmref=false} +\documentclass[sigplan,10pt,review]{llncs} +%% \settopmatter{printfolios=true,printccs=false,printacmref=false} %% For double-blind review submission, w/ CCS and ACM Reference %% \documentclass[acmsmall,review,anonymous]{acmart} %% \settopmatter{printfolios=true} @@ -33,21 +33,22 @@ %%\setcopyright{none} %%\setcopyright{acmcopyright} %%\setcopyright{acmlicensed} -\setcopyright{rightsretained} +%% \setcopyright{rightsretained} %% \copyrightyear{2018} %% If different from \acmYear %% Bibliography style %% FIXME: I hate the way this bibliography looks because I find it %% ridiculously hard to find the entry corresponding to a reference %% like (Blume 2006) in the text. -\bibliographystyle{ACM-Reference-Format} +\newcommand \citet \cite +%% \bibliographystyle{ACM-Reference-Format} %% Citation style %% Note: author/year citations are required for papers published as an %% issue of PACMPL. -\citestyle{acmauthoryear} %% For author/year citations +%% \citestyle{acmauthoryear} %% For author/year citations \usepackage[utf8]{inputenc} -\usepackage{amsmath,amsthm,amssymb,mathtools,stmaryrd} +\usepackage{amsmath,amssymb,mathtools,stmaryrd} \usepackage{mathpartir} \usepackage{mdframed,empheq} \usepackage{parskip} @@ -117,12 +118,16 @@ %% %% contents suppressed with 'anonymous' \author{Stefan Monnier} -\affiliation{ - %% \department{DIRO} - \institution{Université de Montréal - DIRO} - %% \country{Canada} +%% \affiliation{ +%% %% \department{DIRO} +%% \institution{Université de Montréal - DIRO} +%% %% \country{Canada} +%% } +%% \email{monnier(a)iro.umontreal.ca} +\institute{ + Université de Montréal - DIRO \\ + \email{monnier(a)iro.umontreal.ca} } -\email{monnier(a)iro.umontreal.ca} %% \author{Other author} %% \affiliation{ @@ -134,6 +139,8 @@ \date{\today} +\maketitle + %% \input{commands} \begin{abstract} @@ -157,15 +164,15 @@ %% 2012 ACM Computing Classification System (CSS) concepts %% Generate at 'http://dl.acm.org/ccs/ccs.cfm'. -\begin{CCSXML} - %% ... -\end{CCSXML} +%% \begin{CCSXML} +%% %% ... +%% \end{CCSXML} \keywords{Inductive types, compilation, union types} %% Note: \begin{abstract}...\end{abstract} environment must come -%% before \maketitle command -\maketitle +%% before \maketitle command in ACM style. +%% \maketitle %% FIXME: I like to have the table of contents while writing, so I can get %% a quick overview of the structure. Should be removed before submission. @@ -180,7 +187,7 @@ Zombie~\cite{Casinghino14}, and many others. Its design follows that of Scheme, in the sense that it intends to provide a minimalist core language on top of which a nice surface language can be built by metaprogramming. -So the focus of Typer's design is on providing a good core language which is +So a focus of Typer's design is on providing a good core language which is the target of the metaprogramming facilities. Some of the design goals of this language are: \begin{itemize} @@ -1214,7 +1221,7 @@ We can show that this erasure calculus is consistent with the original calculus, and hence that \kw{weaken}, \kw{fold}, and \kw{unfold} can safely be implemented as no-ops: %% -\begin{lemma} +\begin{lemma}[Erasure] \label{lem:erasure} Assuming $ \Jcuc e \tau$, we have: \begin{itemize} @@ -1592,8 +1599,8 @@ We define a translation function $\Ftocic\cdot$ which takes a derivation $\Jcuc{e}{\tau}$ and returns an equivalent expression $e'$ in CIC. As an abuse of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}}$. -\begin{lemma} - Type Preserving translation: Given $\Jcuc e \tau$, we have $\Jcuc \tau s$ and +\begin{lemma}[Type Preserving translation] + Given $\Jcuc e \tau$, we have $\Jcuc \tau s$ and $\Jcic[\Ftocic{\Gamma}] {\Ftocic{\Jcuc e \tau}}{\Ftocic{\Jcuc \tau s}}$. \end{lemma} \begin{proof} @@ -1607,8 +1614,8 @@ of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}} reduction preserves types. \end{proof} -\begin{corollary} - Relative consistency: Assuming there is no $e$ in CIC such that +\begin{corollary}[Relative consistency] + Assuming there is no $e$ in CIC such that $\Jcic[\EmptyCtx]{e}{\bot}$, then there is no $e$ in CUC such that $\Jcuc[\EmptyCtx]{e}{\bot}$. \end{corollary} @@ -1656,6 +1663,9 @@ judgments into the logic: \section{Conclusion} +\newenvironment{acks}{\subsection*{Acknowledgments}}{} +\newcommand \grantsponsor[3] {#2 (#1)} +\newcommand \grantnum[2] {#2} \begin{acks} This work was supported by the \grantsponsor{NSERC}{Natural Sciences and Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} grant @@ -1664,7 +1674,7 @@ judgments into the logic: author and do not necessarily reflect the views of the NSERC. \end{acks} -%% \bibliographystyle{alpha} +\bibliographystyle{alpha} %% \bibliography{typer_theory} \bibliography{/u/monnier/share/misc/all} \end{document} View it on GitLab: https://gitlab.com/monnier/typer/commit/dfd1bc56ea1626d4872ab52cdb3ad5a0deb… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/dfd1bc56ea1626d4872ab52cdb3ad5a0deb… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch report/jfla-2019
by Stefan 25 Oct '18

25 Oct '18

Stefan pushed new branch report/jfla-2019 at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/tree/report/jfla-2019 You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Octobre 2018