--- a/Paper/Paper.thy Tue Sep 28 05:56:11 2010 -0400
+++ b/Paper/Paper.thy Tue Sep 28 08:21:47 2010 -0400
@@ -230,7 +230,10 @@
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
clause states that all the names the function @{text
"bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily
- inspired by the syntax of the Ott-tool \cite{ott-jfp}.
+ inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott
+ has only one binding mode, namely the one where the order of
+ binders matters. Consequently, type-schemes with binding sets
+ of names cannot be modelled in Ott.
However, we will not be able to cope with all specifications that are
allowed by Ott. One reason is that Ott lets the user specify ``empty''
@@ -381,7 +384,10 @@
induction principles that have the variable convention already built in.
The method behind our specification of general binders is taken
from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
- that our specifications make sense for reasoning about $\alpha$-equated terms.
+ that our specifications make sense for reasoning about $\alpha$-equated terms. The main improvement over Ott is that we introduce three binding modes,
+ provide precise definitions for $\alpha$-equivalence and for free
+ variables of our terms, and provide automated proofs inside the
+ Isabelle theorem prover.
\begin{figure}
@@ -929,8 +935,8 @@
\begin{center}
\begin{tabular}{l}
\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
- \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
- \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+ \isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+ \isacommand{bind (res)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
\end{tabular}
\end{center}
@@ -956,8 +962,8 @@
\noindent
Similarly for the other binding modes.
- %Interestingly, in case of \isacommand{bind\_set}
- %and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
+ %Interestingly, in case of \isacommand{bind (set)}
+ %and \isacommand{bind (res)} the binding clauses above will make a difference to the semantics
%of the specifications (the corresponding $\alpha$-equivalence will differ). We will
%show this later with an example.
@@ -972,7 +978,7 @@
alternative binder for the same body). For binders we distinguish between
\emph{shallow} and \emph{deep} binders. Shallow binders are just
labels. The restriction we need to impose on them is that in case of
- \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
+ \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either
refer to atom types or to sets of atom types; in case of \isacommand{bind}
the labels must refer to atom types or lists of atom types. Two examples for
the use of shallow binders are the specification of lambda-terms, where a
@@ -982,7 +988,7 @@
\begin{center}
\begin{tabular}{@ {}cc@ {}}
- \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+ \begin{tabular}{@ {}l@ {\hspace{-2mm}}}
\isacommand{nominal\_datatype} @{text lam} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
\hspace{5mm}$\mid$~@{text "App lam lam"}\\
@@ -994,7 +1000,7 @@
\hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
\hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
- \hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\
+ \hspace{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
\end{tabular}
\end{tabular}
\end{center}
@@ -1004,7 +1010,7 @@
"fset"} to the type of finite sets.
Note that for @{text lam} it does not matter which binding mode we use. The
reason is that we bind only a single @{text name}. However, having
- \isacommand{bind\_set} or \isacommand{bind} in the second case makes a
+ \isacommand{bind (set)} or \isacommand{bind} in the second case makes a
difference to the semantics of the specification (which we will define in the next section).
@@ -1012,8 +1018,8 @@
the atoms in one argument of the term-constructor, which can be bound in
other arguments and also in the same argument (we will call such binders
\emph{recursive}, see below). The binding functions are
- expected to return either a set of atoms (for \isacommand{bind\_set} and
- \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can
+ expected to return either a set of atoms (for \isacommand{bind (set)} and
+ \isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can
be defined by recursion over the corresponding type; the equations
must be given in the binding function part of the scheme shown in
\eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
@@ -1225,11 +1231,11 @@
binding clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of @{text
"fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
"fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
- clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar).
+ clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar).
Suppose the binding clause @{text bc\<^isub>i} is of the form
%
\begin{center}
- \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+ \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
\end{center}
\noindent
@@ -1425,7 +1431,7 @@
empty binding clause of the form
%
\begin{center}
- \mbox{\isacommand{bind\_set} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+ \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
\end{center}
\noindent
@@ -1457,7 +1463,7 @@
Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form
%
\begin{equation}\label{nonempty}
- \mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+ \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
\end{equation}
\noindent
@@ -2113,16 +2119,16 @@
meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
binding clauses. In Ott you specify binding clauses with a single body; we
allow more than one. We have to do this, because this makes a difference
- for our notion of $\alpha$-equivalence in case of \isacommand{bind\_set} and
- \isacommand{bind\_res}. Consider the examples
+ for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and
+ \isacommand{bind (res)}. Consider the examples
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
- \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t s"}\\
+ \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
- \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t"},
- \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "s"}\\
+ \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"},
+ \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
\end{tabular}
\end{center}
@@ -2165,7 +2171,7 @@
In a slightly different domain (programming with dependent types), the
paper \cite{Altenkirch10} presents a calculus with a notion of
- $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
+ $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
has a more operational flavour and calculates a partial (renaming) map.
In this way, the definition can deal with vacuous binders. However, to our
@@ -2182,7 +2188,8 @@
$\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
To specify general binders we used the specifications from Ott, but extended them
in some places and restricted
- them in others so that they make sense in the context of $\alpha$-equated terms.
+ them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not
+ exist in Ott.
We have tried out the extension with terms from Core-Haskell, type-schemes
and the lambda-calculus, and our code
will eventually become part of the next Isabelle distribution.\footnote{For the moment