nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:813ce40078d9
+:a37c65fe10de
 section {* Introduction *}
 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.
+where free and bound variables have names.
-For such terms it derives automatically a reasoning
+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
 \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 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
 \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
-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
+this leads to a rather clumsy formalisation of W. This need of iterating single binders
-for representing multiple binders is also the reason why Nominal Isabelle and other
+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
+in the POPLmark challenge \cite{challenge05}, because also there one would like
-to aviod clumsy reasoning if there were a mechanisms for abstracting several variables
+to bind multiple variables at once.
-at once.
+Binding multiple variables in a single abstraction has interesting properties that are not
-To see this, let us point out some interesting properties of binders abstracting multiple
+captured by iterating single binders. First,
-variables. First, in the case of type-schemes, we do not like to make a distinction
+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$
 \begin{center}
 $\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
 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 terms like
-\begin{center}
+\begin{equation}\label{one}
-$\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$
+\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END
-\end{center}
+\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}
 $\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
 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}
+\begin{equation}\label{two}
-$\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$
+\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END
-\end{center}
+\end{equation}
 \noindent
-we want to bind all variables from the pattern (there might be an arbitrary
+we want to bind all variables from the pattern inside the body of the
-number of them) inside the body of the $\mathtt{let}$, but we also care about
+$\mathtt{let}$, but we also care about the order of these variables, since
-the order of these variables, since we do not want to identify the above term
+we do not want to identify \eqref{two} with
-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
+As a result, we provide three general abstraction mechanisms for binding multiple
-and allow the user to chose which one is intended when formalising a
+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
 a problem that has been pointed out by Pottier in \cite{Pottier06}: in
 $\mathtt{let}$-constructs of the form
 \begin{center}
 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
 \end{center}
 \noindent
-where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes
+where the notation $[\_\!\_].\_\!\_$ indicates that a set of variables becomes
-bound in $s$. In this representation we need additional predicates to ensure
+bound in $s$. In this representation we need additional predicates about terms
-that the two lists are of equal length. This can result into very
+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
 \begin{center}
 \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
-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
+This style of specifying terms and bindings is heavily
-inspired by the Ott-tool \cite{ott-jfp}.
+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,
+specifiactions a reasoning infrastructure for terms that have names for
-\emph{non}-alpha-equated terms. To see the difference, note that working
+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
 \begin{center}
 $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$
 \end{center}
 \noindent
-are not just alpha-equal, but actually equal---we are working with
+are not just alpha-equal, but actually equal. Our insistence on reasoning
-alpha-equivalence classes, but still have that bound variables
+with alpha-equated terms comes from the wealth of experience we gained with
-carry a name.
+the older version of Nominal Isabelle: for non-trivial properties, reasoning
-Our insistence on reasoning with alpha-equated terms comes from the
+about alpha-equated terms is much easier than reasoning with concrete
-wealth of experience we gained with the older version of Nominal
+terms. The fundamental reason for this is that the HOL-logic underlying
-Isabelle: for non-trivial properties,
+Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast,
-reasoning about alpha-equated terms is much easier than reasoning
+replacing ``alpha-equals-by-alpha-equals'' requires a lot of extra work.
-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.
+Although in informal settings a reasoning infrastructure for alpha-equated
+terms that have names is nearly always taken for granted, establishing
-Although a reasoning infrastructure for alpha-equated terms with names
-is in informal reasoning 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
+For every specification we will need to construct a type containing as
-exactly the corresponding alpha-equated terms. For this we use the
+elements exactly those sets containing alpha-equal terms. To do so we use
-standard HOL-technique of defining a new type that has been
+the standard HOL-technique of defining a new type by
-identified as a non-empty subset of an existing type. In our
+identifying a non-empty subset of an existing type. In our
-context we take as the starting point the type of sets of concrete
+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
 can perform in HOL is illustrated by the following picture:
 \cite{HuffmanUrban10}, which we review here briefly to aid the description
 of what follows in the next sections. Two central notions in the nominal
 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
+for each sort. However, in order to simplify the description, we
-shall assume in this paper that there is only a single sort of atoms.
+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
 two-place permutation operation written

changeset 1535	a37c65fe10de
parent 1528	d6ee4a1b34ce
child 1545	f32981105089