diff -r eb95360d6ac6 -r 926245dd5b53 Paper/Paper.thy --- a/Paper/Paper.thy Thu Mar 18 19:39:01 2010 +0100 +++ b/Paper/Paper.thy Thu Mar 18 22:06:28 2010 +0100 @@ -15,16 +15,16 @@ section {* Introduction *} text {* - So far, Nominal Isabelle provided a mechanism to construct - automatically alpha-equated lambda terms sich as + So far, Nominal Isabelle provides a mechanism for constructing + automatically alpha-equated terms such 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 + For such terms it derives automatically a reasoning + infrastructure, which has been used in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result @@ -32,9 +32,9 @@ 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 + However, Nominal Isabelle fared less well in a formalisation of + the algorithm W \cite{UrbanNipkow09}, where types and type-schemes + are of the form \begin{center} \begin{tabular}{l} @@ -43,108 +43,115 @@ \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 + and the quantification abstracts over a finite (possibly empty) set of type variables. + While it is possible to formalise such abstractions by iterating single bindings, + it leads to a very clumsy formalisation of W. This need of iterating single binders + for representing multiple binders is also the reason why Nominal Isabelle and other + theorem provers have not fared extremely well with the more advanced tasks + in the POPLmark challenge \cite{challenge05}, because also there one would be able + to aviod clumsy reasoning if there were a mechanisms for abstracting 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: + To see this, let us point out some interesting properties of binders abstracting multiple + variables. First, in the case of type-schemes, we do not like to make a distinction + about the order of the bound variables. Therefore 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: + but the following two should \emph{not} be 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 + assuming that $x$, $y$ and $z$ are distinct. Moreover, we 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). + In this paper we will give a general abstraction mechanism and associated + notion of alpha-equivalence that can be used to faithfully represent + type-schemes in Nominal Isabelle. The difficulty of finding the right notion + for alpha-equivalence in this case 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 + alway wanted. For example in terms like \begin{center} - $\LET x = 3 \AND y = 2 \IN x \backslash y \END$ + $\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 + we might not care in which order the assignments $x = 3$ and $y = 2$ are + given, but it would be unusual to regard the above term as alpha-equivalent + with \begin{center} - $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$ + $\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. + Therefore we will also provide a separate abstraction mechanism for cases + in which 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 + However, we found that this is still not sufficient for covering language + constructs frequently occuring in programming language research. For example + in $\mathtt{let}$s involving patterns \begin{center} - $\LET (x, y) = (3, 2) \IN x \backslash y \END$ + $\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 + number of them) inside the body of the $\mathtt{let}$, but we also care about + the order of these variables, since we do not want to identify the above term + with \begin{center} - $\LET (y, x) = (3, 2) \IN x \backslash y \END$ + $\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. + As a result, we provide three general abstraction mechanisms for multiple binders + and allow the user to chose which one is intended when formalising a + programming language calculus. - 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 + By providing these general abstraction mechanisms, however, we have to work around + a problem that has been pointed out by Pottier in \cite{Pottier06}: in + $\mathtt{let}$-constructs of the form \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 bind all the $x_i$ in $s$, 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 + as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$-constructor as something like \begin{center} - $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$ + $\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 + where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes 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}). + unintelligible reasoning (see for example~\cite{BengtsonParow09}).