nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:73992021c8f0
+:a7072d498723
 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
-by iterating single binders. First, in the case of type-schemes, we do not
+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{center}
 $\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 perfectly legal instance, and so one needs additional predicates about terms
 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 for example to specify $\mathtt{let}$s
+To avoid this, we will allowto specify for example $\mathtt{let}$s
 as follows
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
-$trm$ & $::=$  & \ldots\\
+$trm$ & $=$  & \ldots\\
 & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]
-$assn$ & $::=$  & $\mathtt{anil}$\\
+$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 auxiliary function identifying the variables to be bound by
-the $\mathtt{let}$. This function can be defined as
+the $\mathtt{let}$. This function can be defined by recursion over $assn$ 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 \mbox{$s\!::\!trm$}, and a binding clause, in this case
-$\mathtt{bind}\;bn\,(a) \IN s$, that states bind all the names the function
+$\mathtt{bind}\;bn\,(a) \IN s$, that states to bind all the names the function
 $bn$ returns 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 specifications a reasoning infrastructure in Isabelle/HOL for
 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
-and the raw terms produced by Ott use names for the bound variables,
+and the raw terms produced by Ott use names for 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$
 \noindent
 are not just alpha-equal, but actually equal. As a
 result, we can only support specifications that make sense on the level of
 alpha-equated terms (offending specifications, which for example bind a variable
-according to a variable bound somewhere else, are not excluded by Ott).  Our
+according to a variable bound somewhere else, are not excluded by Ott, but we
+have to).  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 raw terms. The fundamental reason is that the
+than reasoning with raw 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''
 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
 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
+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
+identifying a non-empty subset of an existing type.   The construction we
-case  we take as the starting point the type of sets of raw
+perform in HOL is illustrated by the following picture:
-terms (the latter being defined as a datatype); identify the
-alpha-equivalence classes according to our alpha-equivalence relation and
-then define the new type as these alpha-equivalence classes.  The construction we
-can perform in HOL is illustrated by the following picture:
 \begin{center}
 \begin{tikzpicture}
 %\draw[step=2mm] (-4,-1) grid (4,1);
 \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
 \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
 \draw (-0.95, 0.3) node[above=0mm] {isomorphism};
-%\rput(3.7,1.75){isomorphism}
 \end{tikzpicture}
+\end{center}
-%%\begin{pspicture}(0.5,0.0)(8,2.5)
-%%\showgrid
+\noindent
-%\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
+We take as the starting point a definition of raw terms (being defined as a
-%\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6}
+datatype in Isabelle/HOL); identify then the
-%\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9)
+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
-%\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5)
+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
-%\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1)
+equivalence relation).\marginpar{\footnotesize Does Ott allow definitions of ``strange'' types?}
-%\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9)
+The fact that we obtain an isomorphism between between the new type and the non-empty
-%\rput(7.3,2.2){$\mathtt{phi}$}
+subset shows that the new type is a faithful representation of alpha-equated terms.
-%\rput(6,1.5){$\lama$}
+That is different for example in the representation of terms using the locally
-%\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}}
+nameless representation of binders: there are non-well-formed terms that need to
-%\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}}
+be excluded by reasoning about a well-formedness predicate.
-%\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}}
-%\rput[c](1.7,1.5){$\lama$}
+The problem with introducing a new type is that in order to be useful
-%\rput(3.7,1.75){isomorphism}
+a resoning infrastructure needs to be ``lifted'' from the underlying type
-%\end{pspicture}
+and subset to the new type. This is usually a tricky task. To ease this task
-\end{center}
+we reimplemented in Isabelle/HOL the quotient package described by Homeier
+\cite{Homeier05}. Gieven that alpha is an equivalence relation, this package
-\noindent
+allows us to automatically lift definitions and theorems involving raw terms
-To ``lift'' the reasoning from the underlying type to the new type
+to definitions and theorems involving alpha-equated terms. This of course
-is usually a tricky task. To ease this task we reimplemented in Isabelle/HOL
+only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
-the quotient package described by Homeier \cite{Homeier05}. This
+Hence we will be able to lift, for instance, the function for free
-re-implementation will automate the proofs we require for our
+variables of raw terms to alpha-equated terms (since this function respects
-reasoning infrastructure over alpha-equated terms.\medskip
+alpha-equivalence), but we will not be able to do this with a bound-variable
+function (since it does not respect alpha-equivalence). As a result, each
+lifting needs some respectulness proofs which we automated.\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
 *}
 section {* A Short Review of the Nominal Logic Work *}
 text {*
-At its core, Nominal Isabelle is based on the nominal logic work by Pitts
+At its core, Nominal Isabelle is an adaption of the nominal logic work by
-\cite{Pitts03}. The implementation of this work are described in
+Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
 \cite{HuffmanUrban10}, which we review here briefly to aid the description
-of what follows in the next sections. Two central notions in the nominal
+of what follows. Two central notions in the nominal logic work are sorted
-logic work are sorted atoms and permutations of atoms. The sorted atoms
+atoms and permutations of atoms. The sorted atoms represent different kinds
-represent different kinds of variables, such as term- and type-variables in
+of variables, such as term- and type-variables in Core-Haskell, and it is
-Core-Haskell, and it is assumed that there is an infinite supply of atoms
+assumed that there is an infinite supply of atoms for each sort. However, in
-for each sort. However, in order to simplify the description, we
+order to simplify the description, we shall assume in what follows that
-shall assume in what follows that there is only a single sort of atoms.
+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
 \end{property}
 *}
-section {* Abstractions *}
+section {* General Binders *}
 text {*
+In order to keep our work managable we like to state general definitions
+and perform proofs inside Isabelle as much as possible, as opposed to write
+custom ML-code that generates appropriate definitions and proofs for each
+instance of a term-calculus. For this, we like to consider pairs
+\begin{equation}\label{three}
+\mbox{@{text "(as, x) :: atom set \<times> \<beta>"}}
+\end{equation}
+\noindent
+consisting of a set of atoms and an object of generic type. The pairs
+are intended to be used for representing binding such as found in
+type-schemes
+\begin{center}
+$\forall \{x_1,\ldots,x_n\}. T$
+\end{center}
+\noindent
+where the atoms $x_1,\ldots,x_n$ is intended to be in \eqref{three} the
+set @{text as} of atoms we want to bind, and $T$, an object-level type, is
+one instance for the generic $x$.
+The first question we have to answer is when we should consider the pairs
+in \eqref{three} as alpha-equivelent? (At the moment we are interested in
+the notion of alpha-equivalence that is \emph{not} preserved by adding
+vacuous binders.) Assuming we are given a free-variable function, say
+\mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then we expect for two alpha-equivelent
+pairs that their sets of free variables aggree. That is
+%
+\begin{equation}\label{four}
+\mbox{@{text "(as, x) \<approx> (bs, y)"} \hspace{2mm}implies\hspace{2mm} @{text "fv(x) - as = fv(y) - bs"}}
+\end{equation}
+\noindent
+Next we expect that there is a permutation, say $p$, that leaves the
+free variables unchanged, but ``moves'' the bound names in $x$ so that
+we obtain $y$ modulo a relation, say @{text "_ R _"}, that characterises when two
+elments of type $\beta$ are equivalent. We also expect that $p$
+makes the binders equal. We can formulate these requirements as: there
+exists a $p$ such that $i)$  @{term "(fv(x) - as) \<sharp>* p"}, $ii)$ @{text "(p \<bullet> x) R y"} and
+$iii)$ @{text "(p \<bullet> as) = bs"}.
+We take now \eqref{four} and the three
 General notion of alpha-equivalence (depends on a free-variable
 function and a relation).
 *}
 section {* Alpha-Equivalence and Free Variables *}
 \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
+also for patiently explaining some of the finer points about the abstract
 definitions and about the implementation of the Ott-tool.
 *}

changeset 1556	a7072d498723
parent 1552	d14b8b21bef2
child 1566	2facd6645599