nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:1694f32b480a
+:014ddf0d7271
 binding \cite{SatoPollack10}.
 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{equation}\label{tysch}
-\begin{tabular}{l}
+\begin{array}{l}
-$T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$
+T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T
-\end{tabular}
+\end{array}
-\end{center}
+\end{equation}
 \noindent
 and the quantification $\forall$ binds a finite (possibly empty) set of
 type-variables.  While it is possible to implement this kind of more general
 binders by iterating single binders, this leads to a rather clumsy
 for example~\cite{BengtsonParow09}). To avoid this, we will allow specifications
 for $\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
 $\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
+allowed by Ott. One reason is that Ott allows ``empty'' specifications
-for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of
+like
-its specifications a reasoning infrastructure in Isabelle/HOL for
+\begin{center}
+$t ::= t\;t \mid \lambda x. t$
+\end{center}
+\noindent
+where no clause for variables is given. Such specifications make sense in
+the context of Coq's type theory (which Ott supports), but not 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
 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
 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
 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).\marginpar{\footnotesize Does Ott allow definitions of ``strange'' types?}
+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
 nameless representation of binders: there are non-well-formed terms that need to
 be excluded by reasoning about a well-formedness predicate.
-The problem with introducing a new type 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 resoning infrastructure needs to be ``lifted'' from the underlying type
+a resoning infrastructure needs to be ``lifted'' from the underlying subset to
-and subset to the new type. This is usually a tricky task. To ease this task
+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
-\cite{Homeier05}. Gieven that alpha is an equivalence relation, this package
+\cite{Homeier05}. Given that alpha is an equivalence relation, this package
 allows us to automatically lift definitions and theorems involving raw terms
 to definitions and theorems involving alpha-equated terms. This of course
 only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
 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
 text {*
 At its core, Nominal Isabelle is an adaption of the nominal logic work by
 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. Two central notions in the nominal logic work are sorted
-atoms and permutations of atoms. The sorted atoms represent different kinds
+atoms and sort-respecting permutations of atoms. The sorts can be used to
-of variables, such as term- and type-variables in Core-Haskell, and it is
+represent different kinds of variables, such as term- and type-variables in
-assumed that there is an infinite supply of atoms for each sort. However, in
+Core-Haskell, and it is assumed that there is an infinite supply of atoms
-order to simplify the description, we shall assume in what follows that
+for each sort. However, in order to simplify the description, we shall
-there is only a single sort of atoms.
+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
 @{text[display,indent=5] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \noindent
 with a generic type in which @{text "\<alpha>"} stands for the type of atoms
-and @{text "\<beta>"} for the type of the objects on which the permutation
+and @{text "\<beta>"} for the type of the object on which the permutation
 acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},
 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}
-and the inverse permutation @{term p} as @{text "- p"}. The permutation
+and the inverse permutation of @{term p} as @{text "- p"}. The permutation
 operation is defined for products, lists, sets, functions, booleans etc
 (see \cite{HuffmanUrban10}).
-The most original aspect of the nominal logic work of Pitts et al is a general
+The most original aspect of the nominal logic work of Pitts is a general
-definition for ``the set of free variables of an object @{text "x"}''.  This
+definition for the notion of ``the set of free variables of an object @{text
-definition is general in the sense that it applies not only to lambda-terms,
+"x"}''.  This notion, written @{term "supp x"}, is general in the sense that
-but also to lists, products, sets and even functions. The definition depends
+it applies not only to lambda-terms alpha-equated or not, but also to lists,
-only on the permutation operation and on the notion of equality defined for
+products, sets and even functions. The definition depends only on the
-the type of @{text x}, namely:
+permutation operation and on the notion of equality defined for the type of
+@{text x}, namely:
 @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
 \noindent
 There is also the derived notion for when an atom @{text a} is \emph{fresh}
 section {* General Binders *}
 text {*
-In order to keep our work managable we like to state general definitions
+In order to keep our work managable we give need to give definitions
-and perform proofs inside Isabelle as much as possible, as opposed to write
+and perform proofs inside Isabelle whereever possible, as opposed to write
-custom ML-code that generates appropriate definitions and proofs for each
+custom ML-code that generates them  for each
-instance of a term-calculus. For this, we like to consider pairs
+instance of a term-calculus. To this end we will first consider pairs
 \begin{equation}\label{three}
-\mbox{@{text "(as, x) :: atom set \<times> \<beta>"}}
+\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
+consisting of a set of atoms and an object of generic type. These pairs
-are intended to be used for representing binding such as found in
+are intended to represent the abstraction or binding of the set $as$
-type-schemes
+in the body $x$ (similarly to type-schemes given in \eqref{tysch}).
-\begin{center}
+The first question we have to answer is when we should consider pairs such as
-$\forall \{x_1,\ldots,x_n\}. T$
+$(as, x)$ and $(bs, y)$ as alpha-equivelent? (At the moment we are interested in
-\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
+vacuous binders.) For this we identify four conditions: i) given a free-variable function
+of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
+need to have the same set of free variables; ii) there must be a permutation,
+say $p$, that leaves the free variables $x$ and $y$ unchanged, but ``moves'' their bound names
+so that we obtain modulo a relation, say @{text "_ R _"},
+two equal terms. We also require that $p$ makes the abstracted sets equal. These
+requirements can be stated formally as
+\begin{center}
+\begin{tabular}{rcl}
+a
+\end{tabular}
+\end{center}
+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"}}
 section {* Adequacy *}
 section {* Related Work *}
+text {*
+Ott is better with list dot specifications; subgrammars
+untyped;
+*}
 section {* Conclusion *}
 text {*
 Complication when the single scopedness restriction is lifted (two
 overlapping permutations)

changeset 1570	014ddf0d7271
parent 1566	2facd6645599
child 1572	0368aef38e6a