--- a/Paper/Paper.thy Mon Mar 22 09:16:25 2010 +0100
+++ b/Paper/Paper.thy Mon Mar 22 10:20:57 2010 +0100
@@ -36,12 +36,12 @@
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}
+ %
+ \begin{equation}\label{tysch}
+ \begin{array}{l}
+ T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T
+ \end{array}
+ \end{equation}
\noindent
and the quantification $\forall$ binds a finite (possibly empty) set of
@@ -157,9 +157,9 @@
\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}
@@ -181,9 +181,21 @@
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
+ 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
+ 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
@@ -247,7 +259,7 @@
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.
@@ -255,11 +267,11 @@
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
- a resoning infrastructure needs to be ``lifted'' from the underlying type
- and subset to the new type. This is usually a tricky task. To ease this task
+ 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 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
- \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.
@@ -287,11 +299,11 @@
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
- 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, we shall assume in what follows that
- there is only a single sort of atoms.
+ atoms and sort-respecting permutations of atoms. The sorts can be used to
+ 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, we shall
+ assume in what follows that there is only a single sort of atoms.
Permutations are bijective functions from atoms to atoms that are
@@ -302,19 +314,20 @@
\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
- definition for ``the set of free variables of an object @{text "x"}''. This
- definition is general in the sense that it applies not only to lambda-terms,
- but also to lists, products, sets and even functions. The definition depends
- only on the permutation operation and on the notion of equality defined for
- the type of @{text x}, namely:
+ The most original aspect of the nominal logic work of Pitts is a general
+ definition for the notion of ``the set of free variables of an object @{text
+ "x"}''. This notion, written @{term "supp x"}, is general in the sense that
+ it applies not only to lambda-terms alpha-equated or not, but also to lists,
+ products, sets and even functions. The definition depends only on the
+ 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]}
@@ -350,33 +363,39 @@
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
+ In order to keep our work managable we give need to give definitions
+ and perform proofs inside Isabelle whereever possible, as opposed to write
+ custom ML-code that generates them for each
+ 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
- are intended to be used for representing binding such as found in
- type-schemes
+ consisting of a set of atoms and an object of generic type. These pairs
+ are intended to represent the abstraction or binding of the set $as$
+ in the body $x$ (similarly to type-schemes given in \eqref{tysch}).
+
+ The first question we have to answer is when we should consider pairs such as
+ $(as, x)$ and $(bs, y)$ as alpha-equivelent? (At the moment we are interested in
+ the notion of alpha-equivalence that is \emph{not} preserved by adding
+ 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}
- $\forall \{x_1,\ldots,x_n\}. T$
+ \begin{tabular}{rcl}
+ a
+ \end{tabular}
\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
+ 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
%
@@ -420,6 +439,14 @@
section {* Related Work *}
+text {*
+ Ott is better with list dot specifications; subgrammars
+
+ untyped;
+
+*}
+
+
section {* Conclusion *}
text {*