nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:2789dd26171a
+:f32981105089
 \end{center}
 \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
 for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
 used by Pollack for formalisations in the locally-nameless approach to
 $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$
 \end{tabular}
 \end{center}
 \noindent
-and the quantification binds a finite (possibly empty) set of type-variables.
+and the quantification binds at once a finite (possibly empty) set of type-variables.
-While it is possible to formalise such abstractions by iterating single bindings,
+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. This need of iterating single binders
+this leads to a rather clumsy formalisation of W. The need of iterating single binders
-in order to representing multiple binders is also one reason why Nominal Isabelle and other
+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
 type-schemes as alpha-equivalent
 $\forall \{x\}. x \rightarrow y  \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$
 \end{center}
 \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
 \begin{equation}\label{one}
 \begin{center}
 $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$
 \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
+However, we found that this is still not sufficient for dealing with language
-constructs frequently occuring in programming language research. For example
+constructs frequently occurring in programming language research. For example
 in $\mathtt{let}$s involving patterns
 \begin{equation}\label{two}
 \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END
 \end{equation}
 \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 binding multiple
+As a result, we provide three general binding mechanisms each of which binds multiple
-variables and allow the user to chose which one is intended when formalising a
+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
 \begin{center}
 $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
 \begin{center}
 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
 \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}
 \end{center}
 \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}
 $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$
 \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
+However, we will not be able to deal with all specifications that are
-Ott. One reason is that we establish the reasoning infrastructure for
+allowed by Ott. One reason is that we establish the reasoning infrastructure
-alpha-\emph{equated} terms. In contrast, Ott produces for a subset of its
+for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of
-specifiactions a reasoning infrastructure for terms that have names for
+its specifications a reasoning infrastructure in Isabelle for
-bound variables, but these terms are concrete, \emph{non}-alpha-equated terms. To see
+\emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
-the difference, note that working
+and the concrete terms produced by Ott use names for the bound variables,
-with alpha-equated terms means that the two type-schemes with $x$, $y$ and
+there is a key difference: working with alpha-equated terms means that the
-$z$ being distinct
+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
+are not just alpha-equal, but actually equal (note the ``=''-sign). Our insistence
-with alpha-equated terms comes from the wealth of experience we gained with
+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
+terms. The fundamental reason is that the HOL-logic underlying
-Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast,
+Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast replacing
-replacing ``alpha-equals-by-alpha-equals'' requires a lot of extra work.
+``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
+case  we take as the starting point the type of sets of concrete
-terms (the latter being defined as datatypes). Then quotient these
+terms (the latter being defined as a datatype). Then identify the
-sets according to our alpha-equivalence relation and then identifying
+alpha-equivalence classes according to our alpha-equivalence relation and
-the new type as these alpha-equivalence classes.  The construction we
+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)
 %%\showgrid
 %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
 \noindent
 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for
 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.
 *}

changeset 1545	f32981105089
parent 1535	a37c65fe10de
child 1550	66d388a84e3c