diff -r 62d6f7acc110 -r 6ac75fd979d4 Paper/Paper.thy --- a/Paper/Paper.thy Thu Mar 18 16:22:10 2010 +0100 +++ b/Paper/Paper.thy Thu Mar 18 18:43:03 2010 +0100 @@ -15,17 +15,131 @@ section {* Introduction *} text {* + So far, Nominal Isabelle provided a mechanism to construct + automatically alpha-equated lambda terms sich as - It has not yet fared so well in the POPLmark challenge - as the second part contain a formalisation of records - where ... + \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} - The difficulty can be appreciated by considering that the - definition given by Leroy in \cite{Leroy92} is incorrect (it omits a - side-condition). + \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 - Examples: type-schemes, Spi-calculus + \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 represent the $\mathtt{let}$ + as something + + + + + Contributions: We provide definitions for when terms involving general bindings are alpha-equivelent. @@ -129,6 +243,18 @@ 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 *} @@ -138,6 +264,11 @@ section {* Conclusion *} text {* + Complication when the single scopedness restriction is lifted (two + overlapping permutations) +*} + +text {* TODO: function definitions: \medskip