nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:e33e37fd4c7d
+:ac69ed8303cc
 section {* Introduction *}
 text {*
 So far, Nominal Isabelle provides a mechanism for constructing
-alpha-equated terms such as
+alpha-equated terms, for example
 \begin{center}
 $t ::= x \mid t\;t \mid \lambda x. t$
 \end{center}
 \noindent
 where free and bound variables have names.  For such terms Nominal Isabelle
-derives automatically a reasoning infrastructure, which has been used
+derives automatically a reasoning infrastructure that  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
 \noindent
 where $z$ does not occur freely in the type.
 In this paper we will give a general binding mechanism and associated
 notion of alpha-equivalence that can be used to faithfully represent
 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
+for alpha-equivalence can be appreciated in this case 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
 always wanted. For example in terms like
 %
 \noindent
 The scope of the binding is indicated by labels given to the types, for
 example \mbox{$s\!::\!trm$}, and a binding clause, in this case
 $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the
-function $bn\,(a)$ returns.  This style of specifying terms and bindings is
+function call $bn\,(a)$ returns.  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 Ott allows ``empty'' specifications
 like
 $t ::= t\;t \mid \lambda x. t$
 \end{center}
 \noindent
 where no clause for variables is given. Such specifications make some sense in
-the context of Coq's type theory (which Ott supports), but not at al in a HOL-based
+the context of Coq's type theory (which Ott supports), but not at all in a HOL-based
-theorem prover where every datatype must have a non-empty set-theoretic model.
+environment where every datatype must have a non-empty set-theoretic model.
 Another reason is that we establish the reasoning infrastructure
 for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning
 infrastructure in Isabelle/HOL for
 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
 HOL-logic underlying Nominal Isabelle allows us to replace
 ``equals-by-equals''. In contrast replacing ``alpha-equals-by-alpha-equals''
 in a representation based on raw terms requires a lot of extra reasoning work.
 Although in informal settings a reasoning infrastructure for alpha-equated
-terms (that have names for bound variables) is nearly always taken for granted, establishing
+terms is nearly always taken for granted, establishing
 it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task.
 For every specification we will need to construct a type containing as
 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.   The construction we
-perform in HOL is illustrated by the following picture:
+perform in HOL can be illustrated by the following picture:
 \begin{center}
 \begin{tikzpicture}
 %\draw[step=2mm] (-4,-1) grid (4,1);
 \end{center}
 \noindent
 We take as the starting point a definition of raw terms (defined as a
 datatype in Isabelle/HOL); identify then the
-alpha-equivalence classes in the type of sets of raw terms, according to our
+alpha-equivalence classes in the type of sets of raw terms according to our
 alpha-equivalence relation and finally define the new type as these
 alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are
-definable as datatype in Isabelle/HOL and the fact that our relation for alpha is an
+definable as datatype in Isabelle/HOL and the fact that our relation for
-equivalence relation).
+alpha-equivalence is indeed an equivalence relation).
-The fact that we obtain an isomorphism between between the new type and the non-empty
+The fact that we obtain an isomorphism between the new type and the non-empty
 subset shows that the new type is a faithful representation of alpha-equated terms.
 That is not the case for example in the representation of terms using the locally
-nameless representation of binders \cite{McKinnaPollack99}: there are ``junk'' terms that need to
+nameless representation of binders \cite{McKinnaPollack99}: in this representation
+there are ``junk'' terms that need to
 be excluded by reasoning about a well-formedness predicate.
 The problem with introducing a new type in Isabelle/HOL is that in order to be useful,
 a reasoning infrastructure needs to be ``lifted'' from the underlying subset to
-the new type. This is usually a tricky and arduous task. To ease it
+the new type. This is usually a tricky and arduous task. To ease it,
 we re-implemented in Isabelle/HOL the quotient package described by Homeier
 \cite{Homeier05}. This package
 allows us to  lift definitions and theorems involving raw terms
-to definitions and theorems involving alpha-equated terms. For example
+to definitions and theorems involving alpha-equated, terms. For example
 if we define the free-variable function over lambda terms
 \begin{center}
 $\fv(x) = \{x\}$\hspace{10mm}
 $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]
 \end{center}
 \noindent
 (Note that this means also the term-constructors for variables, applications
 and lambda are lifted to the quotient level.)  This construction, of course,
-only works if alpha is an equivalence relation, and the definitions and theorems
+only works if alpha-equivalence is an equivalence relation, and the
-are respectful w.r.t.~alpha-equivalence.  Hence we will not be able to lift this
+definitions and theorems are respectful w.r.t.~alpha-equivalence.  Hence we
-a bound-variable function to alpha-equated terms (since it does not respect
+will not be able to lift a bound-variable function to alpha-equated terms
-alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness
+(since it does not respect alpha-equivalence). To sum up, every lifting of
-properties. These proofs we are able automate and therefore establish a
+theorems to the quotient level needs proofs of some respectfulness
-useful reasoning infrastructure for alpha-equated lambda terms.\medskip
+properties. In the paper we show that we are able to automate these
+proofs and therefore can establish a reasoning infrastructure for
+alpha-equated terms.\medskip
 \noindent
 {\bf Contributions:}  We provide new definitions for when terms
 involving multiple binders are alpha-equivalent. These definitions are
-inspired by earlier work of Pitts \cite{}. By means of automatic
+inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 proofs, we establish a reasoning infrastructure for alpha-equated
 terms, including properties about support, freshness and equality
-conditions for alpha-equated terms. We re also able to derive, at the moment
+conditions for alpha-equated terms. We are also able to derive, at the moment
-only manually, for these terms a strong induction principle that
+only manually, strong induction principles that
-has the variable convention already built in.
+have the variable convention already built in.
 *}
 section {* A Short Review of the Nominal Logic Work *}
 text {*
 of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$
 written as follows:
 \begin{center}
 \begin{tabular}{l}
-\isacommand{nominal\_datatype} $ty_1 =$\\
+\isacommand{nominal\_datatype} $ty_{\alpha{}1} =$\\
-\isacommand{and} $ty_2 =$\\
+\isacommand{and} $ty_{\alpha{}2} =$\\
 $\ldots$\\
-\isacommand{and} $ty_n =$\\
+\isacommand{and} $ty_{\alpha{}}n =$\\
 $\ldots$\\
 \isacommand{with}\\
 $\ldots$\\
 \end{tabular}
 \end{center}

changeset 1607	ac69ed8303cc
parent 1587	b6da798cef68
child 1611	091f373baae9