(*<*)theory Paperimports "../Nominal/Test" "LaTeXsugar"beginnotation (latex output) swap ("'(_ _')" [1000, 1000] 1000) and fresh ("_ # _" [51, 51] 50) and fresh_star ("_ #* _" [51, 51] 50) and supp ("supp _" [78] 73) and uminus ("-_" [78] 73) and If ("if _ then _ else _" 10)(*>*)section {* Introduction *}text {* So far, Nominal Isabelle provided a mechanism to construct automatically alpha-equated lambda terms sich as \begin{center} $t ::= x \mid t\;t \mid \lambda x. t$ \end{center} \noindent For such calculi, it derived automatically a convenient reasoning infrastructure. With this it has been used to formalise an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for formalisations in the locally-nameless approach to binding \cite{SatoPollack10}. However, Nominal Isabelle has fared less well in a formalisation of the algorithm W \cite{UrbanNipkow09} where types and type-schemes are represented by \begin{center} \begin{tabular}{l} $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ \end{tabular} \end{center} \noindent While it is possible to formalise the finite set of variables that are abstracted in a type-scheme by iterating single abstractions, it leads to a very clumsy formalisation. This need of iterating single binders for representing multiple binders is also the reason why Nominal Isabelle and other theorem provers have so far not fared very well with the more advanced tasks in the POPLmark challenge, because also there one would like to abstract several variables at once. There are interesting points to note with binders that abstract multiple variables. First in the case of type-schemes we do not like to make a distinction about the order of the binders. So we would like to regard the following two type-schemes as alpha-equivalent: \begin{center} $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ \end{center} \noindent but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} alpha-equivalent: \begin{center} $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ \end{center} \noindent However we do like to regard type-schemes as alpha-equivalent, if they differ only on \emph{vacuous} binders, such as \begin{center} $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ \end{center} \noindent In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence which can be used to represent type-schemes. The difficulty in finding the notion of alpha-equivalence can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). However, the notion of alpha-equivalence that is preserved by vacuous binders is not alway wanted. For example in constructs like \begin{center} $\LET x = 3 \AND y = 2 \IN x \backslash y \END$ \end{center} \noindent we might not care in which order the associations $x = 3$ and $y = 2$ are given, but it would be unusual to regard this term as alpha-equivalent with \begin{center} $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$ \end{center} \noindent We will provide a separate abstraction mechanism for this case where the order of binders does not matter, but the ``cardinality'' of the binders has to be the same. However, this is still not sufficient for covering language constructs frequently occuring in programming language research. For example in patters like \begin{center} $\LET (x, y) = (3, 2) \IN x \backslash y \END$ \end{center} \noindent we want to bind all variables from the pattern (there might be an arbitrary number of them) inside the body of the let, but we also care about the order of these variables, since we do not want to identify this term with \begin{center} $\LET (y, x) = (3, 2) \IN x \backslash y \END$ \end{center} \noindent Therefore we have identified three abstraction mechanisms for multiple binders and allow the user to chose which one is intended. By providing general abstraction mechanisms that allow the binding of multiple variables, we have to work around aproblem that has been first pointed out by Pottier in \cite{Pottier}: in let-constructs such as \begin{center} $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ \end{center} \noindent where the $x_i$ are bound in $s$. In this term we might not care about the order in which the $x_i = t_i$ are given, but we do care about the information that there are as many $x_i$ as there are $t_i$. We lose this information if we specify the $\mathtt{let}$-constructor as something like \begin{center} $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$ \end{center} \noindent where the $[\_].\_$ indicates that a list of variables become bound in $s$. In this representation we need additional predicates to ensure that the two lists are of equal length. This can result into very elaborate reasoning (see \cite{BengtsonParow09}). Contributions: We provide definitions for when terms involving general bindings are alpha-equivelent. %\begin{center} %\begin{pspicture}(0.5,0.0)(8,2.5) %%\showgrid %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9) %\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5) %\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1) %\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9) %\rput(7.3,2.2){$\mathtt{phi}$} %\rput(6,1.5){$\lama$} %\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}} %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}} %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}} %\rput[c](1.7,1.5){$\lama$} %\rput(3.7,1.75){isomorphism} %\end{pspicture} %\end{center} quotient package \cite{Homeier05}*}section {* A Short Review of the Nominal Logic Work *}text {* At its core, Nominal Isabelle is based on the nominal logic work by Pitts \cite{Pitts03}. The implementation of this work are described in \cite{HuffmanUrban10}, which we review here briefly to aid the description of what follows in the next sections. Two central notions in the nominal logic work are sorted atoms and permutations of atoms. The sorted atoms represent different kinds of variables, such as term- and type-variables in Core-Haskell, and it is assumed that there is an infinite supply of atoms for each sort. However, in order to simplify the description of our work, we shall assume in this paper that there is only a single sort of atoms. Permutations are bijective functions from atoms to atoms that are the identity everywhere except on a finite number of atoms. There is a two-place permutation operation written @{text[display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} \noindent with a generic type in which @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type of the objects on which the permutation acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"}, the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}} and the inverse permutation @{term p} as @{text "- p"}. The permutation operation is defined for products, lists, sets, functions, booleans etc (see \cite{HuffmanUrban10}). The most original aspect of the nominal logic work of Pitts et al is a general definition for ``the set of free variables of an object @{text "x"}''. This definition is general in the sense that it applies not only to lambda-terms, but also to lists, products, sets and even functions. The definition depends only on the permutation operation and on the notion of equality defined for the type of @{text x}, namely: @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]} \noindent There is also the derived notion for when an atom @{text a} is \emph{fresh} for an @{text x}, defined as @{thm[display,indent=5] fresh_def[no_vars]} \noindent We also use for sets of atoms the abbreviation @{thm (lhs) fresh_star_def[no_vars]} defined as @{thm (rhs) fresh_star_def[no_vars]}. A striking consequence of these definitions is that we can prove without knowing anything about the structure of @{term x} that swapping two fresh atoms, say @{text a} and @{text b}, leave @{text x} unchanged. \begin{property} @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} \end{property} \noindent For a proof see \cite{HuffmanUrban10}. \begin{property} @{thm[mode=IfThen] at_set_avoiding[no_vars]} \end{property}*}section {* Abstractions *}text {* General notion of alpha-equivalence (depends on a free-variable function and a relation).*}section {* Alpha-Equivalence and Free Variables *}text {* Restrictions \begin{itemize} \item non-emptyness \item positive datatype definitions \item finitely supported abstractions \item respectfulness of the bn-functions\bigskip \item binders can only have a ``single scope'' \end{itemize}*}section {* Examples *}section {* Adequacy *}section {* Related Work *}section {* Conclusion *}text {* Complication when the single scopedness restriction is lifted (two overlapping permutations)*}text {* TODO: function definitions: \medskip \noindent {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the many discussions about Nominal Isabelle. We thank Peter Sewell for making the informal notes \cite{SewellBestiary} available to us and also for explaining some of the finer points of the OTT-tool.*}(*<*)end(*>*)