diff -r 0d845717f181 -r 2789dd26171a Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 19 10:24:16 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 19 10:24:49 2010 +0100 @@ -16,15 +16,15 @@ text {* So far, Nominal Isabelle provides a mechanism for constructing - automatically alpha-equated terms such as + alpha-equated terms such as \begin{center} $t ::= x \mid t\;t \mid \lambda x. t$ \end{center} \noindent - where bound variables have a name. - For such terms it derives automatically a reasoning + where free and bound variables have names. + For such terms Nominal Isabelle 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 @@ -33,7 +33,7 @@ used by Pollack for formalisations in the locally-nameless approach to binding \cite{SatoPollack10}. - However, Nominal Isabelle fared less well in a formalisation of + However, Nominal Isabelle has fared less well in a formalisation of the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are of the form @@ -44,17 +44,17 @@ \end{center} \noindent - and the quantification abstracts over a finite (possibly empty) set of type variables. + and the quantification binds 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 + this leads to a rather clumsy formalisation of W. This need of iterating single binders + in order to representing multiple binders is also one 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. + in the POPLmark challenge \cite{challenge05}, because also there one would like + to bind multiple variables at once. - 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 + Binding multiple variables in a single abstraction has interesting properties that are not + captured by iterating single binders. 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 @@ -78,6 +78,7 @@ \end{center} \noindent + where $z$ does not occur freely in the type. 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 @@ -89,13 +90,13 @@ However, the notion of alpha-equivalence that is preserved by vacuous binders is not alway wanted. For example in terms like - \begin{center} - $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$ - \end{center} + \begin{equation}\label{one} + \LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END + \end{equation} \noindent 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 + given, but it would be unusual to regard \eqref{one} as alpha-equivalent with \begin{center} @@ -105,29 +106,28 @@ \noindent 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. + binders has to agree. 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$ - \end{center} + \begin{equation}\label{two} + \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END + \end{equation} \noindent - we want to bind all variables from the pattern (there might be an arbitrary - 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 + we want to bind all variables from the pattern inside the body of the + $\mathtt{let}$, but we also care about the order of these variables, since + we do not want to identify \eqref{two} with \begin{center} $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$ \end{center} \noindent - 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 + As a result, we provide three general abstraction mechanisms for binding multiple + variables and allow the user to chose which one is intended when formalising a programming language calculus. By providing these general abstraction mechanisms, however, we have to work around @@ -149,9 +149,9 @@ \end{center} \noindent - 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 + where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes + bound in $s$. In this representation we need additional predicates about terms + to ensure that the two lists are of equal length. This can result into very unintelligible reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will allow for example specifications of $\mathtt{let}$s as follows @@ -168,21 +168,22 @@ \noindent where $assn$ is an auxiliary type representing a list of assignments and $bn$ an auxilary function identifying the variables to be bound by - the $\mathtt{let}$, given by + the $\mathtt{let}$. This function can be defined as \begin{center} $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ \end{center} \noindent - This style of specifications for term-calculi with multiple binders is heavily - inspired by the Ott-tool \cite{ott-jfp}. + This style of specifying terms and bindings is heavily + inspired by the syntax of the Ott-tool \cite{ott-jfp}. - We will not be able to deal with all specifications that are allowed by + However, we will not be able to deal with all specifications that are allowed by Ott. One reason is that we establish the reasoning infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of its - specifiactions a reasoning infrastructure involving concrete, - \emph{non}-alpha-equated terms. To see the difference, note that working + specifiactions a reasoning infrastructure for terms that have names for + bound variables, but these terms are concrete, \emph{non}-alpha-equated terms. To see + the difference, note that working with alpha-equated terms means that the two type-schemes with $x$, $y$ and $z$ being distinct @@ -191,25 +192,23 @@ \end{center} \noindent - are not just alpha-equal, but actually equal---we are working with - alpha-equivalence classes, but still have that bound variables - carry a name. - Our insistence on reasoning with alpha-equated terms comes from the - wealth of experience we gained with the older version of Nominal - Isabelle: for non-trivial properties, - reasoning about alpha-equated terms is much easier than reasoning - with concrete terms. The fundamental reason is that the HOL-logic - underlying Nominal Isabelle allows us to replace ``equals-by-equals''. - Replacing ``alpha-equals-by-alpha-equals'' requires a lot of work. + are not just alpha-equal, but actually equal. Our insistence on reasoning + with alpha-equated terms comes from the wealth of experience we gained with + the older version of Nominal Isabelle: for non-trivial properties, reasoning + about alpha-equated terms is much easier than reasoning with concrete + terms. The fundamental reason for this is that the HOL-logic underlying + Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast, + replacing ``alpha-equals-by-alpha-equals'' requires a lot of extra work. + - Although a reasoning infrastructure for alpha-equated terms with names - is in informal reasoning nearly always taken for granted, establishing + Although in informal settings a reasoning infrastructure for alpha-equated + terms that have names is nearly always taken for granted, establishing it automatically in a theorem prover is a rather non-trivial task. - For every specification we will construct a type that contains - exactly the corresponding alpha-equated terms. For this we use the - standard HOL-technique of defining a new type that has been - identified as a non-empty subset of an existing type. In our - context we take as the starting point the type of sets of concrete + For every specification we will need to construct a type containing as + elements exactly those sets containing alpha-equal terms. To do so we use + the standard HOL-technique of defining a new type by + identifying a non-empty subset of an existing type. In our + we take as the starting point the type of sets of concrete terms (the latter being defined as datatypes). Then quotient these sets according to our alpha-equivalence relation and then identifying the new type as these alpha-equivalence classes. The construction we @@ -271,8 +270,8 @@ 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. + for each sort. However, in order to simplify the description, we + shall assume in what follows 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