nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:0368aef38e6a
+:8466fe2216da
 why Nominal Isabelle and similar theorem provers that only provide
 mechanisms for binding single variables 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 has interesting properties that are not captured
+Binding multiple variables has interesting properties that cannot be captured
-by iterating single binders. For example in the case of type-schemes we do not
+easily by iterating single binders. For example 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{equation}\label{ex1}
 \forall \{x, y\}. x \rightarrow y  \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x
 where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound
 in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
 would be a perfectly legal instance. To exclude such terms an additional
 predicate about well-formed terms is needed in order to ensure that the two
 lists are of equal length. This can result into very messy reasoning (see
-for example~\cite{BengtsonParow09}). To avoid this, we will allow specifications
+for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
 for $\mathtt{let}$s as follows
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
 $trm$ & $::=$  & \ldots\\
 & $\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 auxiliary function identifying the variables to be bound by
 the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows
 \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 \mbox{$s\!::\!trm$}, and a binding clause, in this case
-$\mathtt{bind}\;bn\,(a) \IN s$, that states to bind all the names the function
+$\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the
-$bn$ returns in $s$.  This style of specifying terms and bindings is heavily
+function $bn\,(a)$ returns.  This style of specifying terms and bindings is
-inspired by the syntax of the Ott-tool \cite{ott-jfp}.
+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
 \begin{center}
 $t ::= t\;t \mid \lambda x. t$
 \end{center}
 \noindent
-where no clause for variables is given. Such specifications make sense in
+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 in a HOL-based
+the context of Coq's type theory (which Ott supports), but not at al in a HOL-based
 theorem prover 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
 \end{tikzpicture}
 \end{center}
 \noindent
-We take as the starting point a definition of raw terms (being defined as a
+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 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
 equivalence relation).
 The fact that we obtain an isomorphism between between the new type and the non-empty
 subset shows that the new type is a faithful representation of alpha-equated terms.
-That is different for example in the representation of terms using the locally
+That is not the case for example in the representation of terms using the locally
-nameless representation of binders: there are non-well-formed terms that need to
+nameless representation of binders \cite{McKinnaPollack99}: 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
+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
-we reimplemented in Isabelle/HOL the quotient package described by Homeier
+we re-implemented in Isabelle/HOL the quotient package described by Homeier
-\cite{Homeier05}. Given that alpha is an equivalence relation, this package
+\cite{Homeier05}. This package
-allows us to automatically lift definitions and theorems involving raw terms
+allows us to  lift definitions and theorems involving raw terms
-to definitions and theorems involving alpha-equated terms. This of course
+to definitions and theorems involving alpha-equated terms. For example
-only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
+if we define the free-variable function over lambda terms
-Hence we will be able to lift, for instance, the function for free
-variables of raw terms to alpha-equated terms (since this function respects
+\begin{center}
-alpha-equivalence), but we will not be able to do this with a bound-variable
+$\fv(x) = \{x\}$\hspace{10mm}
-function (since it does not respect alpha-equivalence). As a result, each
+$\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]
-lifting needs some respectfulness proofs which we automated.\medskip
+$\fv(\lambda x.t) = \fv(t) - \{x\}$
+\end{center}
+\noindent
+then with not too great effort we obtain a function $\fv_\alpha$
+operating on quotients, or alpha-equivalence classes of terms, as follows
+\begin{center}
+$\fv_\alpha(x) = \{x\}$\hspace{10mm}
+$\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]
+$\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$
+\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
+are respectful w.r.t.~alpha-equivalence.  Hence we will not be able to lift this
+a bound-variable function to alpha-equated terms (since it does not respect
+alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness
+properties. These proofs we are able automate and therefore establish a
+useful reasoning infrastructure for alpha-equated lambda 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
 \item non-emptiness
 \item positive datatype definitions
 \item finitely supported abstractions
 \item respectfulness of the bn-functions\bigskip
 \item binders can only have a ``single scope''
+\item all bindings must have the same mode
 \end{itemize}
 *}
 section {* Examples *}
 many discussions about Nominal Isabelle. We thank Peter Sewell for
 making the informal notes \cite{SewellBestiary} available to us and
 also for patiently explaining some of the finer points about the abstract
 definitions and about the implementation of the Ott-tool.
+Lookup: Merlin paper by James Cheney; Mark Shinwell PhD
+Future work: distinct list abstraction
 *}
 (*<*)

changeset 1577	8466fe2216da
parent 1572	0368aef38e6a
child 1579	5b0bdd64956e