diff -r 2789dd26171a -r f32981105089 Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 19 10:24:49 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 19 12:31:17 2010 +0100 @@ -25,7 +25,7 @@ \noindent 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 + infrastructure, which has been used successfully 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 @@ -44,15 +44,15 @@ \end{center} \noindent - and the quantification binds a finite (possibly empty) set of type-variables. - While it is possible to formalise such abstractions by iterating single bindings, - 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 + and the quantification binds at once a finite (possibly empty) set of type-variables. + While it is possible to implement this kind of more general binders by iterating single binders, + this leads to a rather clumsy formalisation of W. The need of iterating single binders + is also one reason why Nominal Isabelle and similar theorem provers have not fared extremely well with the more advanced tasks in the POPLmark challenge \cite{challenge05}, because also there one would like to bind multiple variables at once. - Binding multiple variables in a single abstraction has interesting properties that are not + Binding multiple variables 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 @@ -79,14 +79,12 @@ \noindent where $z$ does not occur freely in the type. - In this paper we will give a general abstraction mechanism and associated + In this paper we will give a general binding 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 + this kind of binding 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 terms like @@ -104,12 +102,12 @@ \end{center} \noindent - Therefore we will also provide a separate abstraction mechanism for cases + Therefore we will also provide a separate binding mechanism for cases in which the order of binders does not matter, but the ``cardinality'' of the 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 + However, we found that this is still not sufficient for dealing with language + constructs frequently occurring in programming language research. For example in $\mathtt{let}$s involving patterns \begin{equation}\label{two} @@ -126,11 +124,11 @@ \end{center} \noindent - 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 + As a result, we provide three general binding mechanisms each of which binds multiple + variables at once, and we let the user chose which one is intended when formalising a programming language calculus. - By providing these general abstraction mechanisms, however, we have to work around + By providing these general binding 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 @@ -149,17 +147,17 @@ \end{center} \noindent - where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes + where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become 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 + To avoid this, we will allow to specify $\mathtt{let}$s as follows \begin{center} \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} $trm$ & $::=$ & \ldots\\ - & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;t\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN t$\\[1mm] + & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] $assn$ & $::=$ & $\mathtt{anil}$\\ & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$ \end{tabular} @@ -167,7 +165,7 @@ \noindent where $assn$ is an auxiliary type representing a list of assignments - and $bn$ an auxilary function identifying the variables to be bound by + and $bn$ an auxiliary function identifying the variables to be bound by the $\mathtt{let}$. This function can be defined as \begin{center} @@ -175,50 +173,47 @@ \end{center} \noindent + The scope of the binding is indicated by labels given to the types, for example + $s\!::\!trm$, and a binding clause $\mathtt{bind}\;bn\,(a) \IN s$. This style of specifying terms and bindings is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. - 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 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 + 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 specifications a reasoning infrastructure in Isabelle for + \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms + and the concrete terms produced by Ott use names for the bound variables, + there is a key difference: working with alpha-equated terms means that the + two type-schemes with $x$, $y$ and $z$ being distinct \begin{center} $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ \end{center} \noindent - 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 + are not just alpha-equal, but actually equal (note the ``=''-sign). 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. + terms. The fundamental reason is that the HOL-logic underlying + Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast replacing + ``alpha-equals-by-alpha-equals'' in a term calculus requires a lot of extra reasoning work. Although in informal settings a reasoning infrastructure for alpha-equated - terms that have names is nearly always taken for granted, establishing + terms (that have names for bound variables) is nearly always taken for granted, establishing it automatically in a theorem prover is a rather non-trivial task. 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 + elements the alpha-equated 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 + case we take as the starting point the type of sets of concrete + terms (the latter being defined as a datatype). Then identify the + alpha-equivalence classes according to our alpha-equivalence relation and + then identify the new type as these alpha-equivalence classes. The construction we can perform in HOL is illustrated by the following picture: - - - - Contributions: We provide definitions for when terms - involving general bindings are alpha-equivelent. - + \begin{center} figure %\begin{pspicture}(0.5,0.0)(8,2.5) @@ -370,7 +365,7 @@ 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 about the abstract - definitions and about the implmentation of the Ott-tool. + definitions and about the implementation of the Ott-tool. *}