--- a/Paper/Paper.thy Tue Oct 05 21:48:31 2010 +0100
+++ b/Paper/Paper.thy Wed Oct 06 08:09:40 2010 +0100
@@ -448,12 +448,12 @@
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
- in which the generic type @{text "\<beta>"} stands for the type of the object
+ where the generic type @{text "\<beta>"} stands for the type of the object
over 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 of @{term p} as @{text "- p"}. The permutation
- operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};
+ operation is defined over the type-hierarchy \cite{HuffmanUrban10};
for example permutations acting on products, lists, sets, functions and booleans is
given by:
%
@@ -611,7 +611,7 @@
@{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
Most properties given in this section are described in detail in \cite{HuffmanUrban10}
- and of course all are formalised in Isabelle/HOL. In the next sections we will make
+ and all are formalised in Isabelle/HOL. In the next sections we will make
extensive use of these properties in order to define $\alpha$-equivalence in
the presence of multiple binders.
*}
@@ -737,13 +737,13 @@
\noindent
(similarly for $\approx_{\,\textit{abs\_res}}$
and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
- relations and equivariant.
+ relations. %% and equivariant.
\begin{lemma}\label{alphaeq}
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
- and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
- "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
- bs, p \<bullet> y)"} (similarly for the other two relations).
+ and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if
+ %@{term "abs_set (as, x) (bs, y)"} then also
+ %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
\end{lemma}
\begin{proof}
@@ -929,15 +929,15 @@
annotated on the types are optional. Their purpose is to be used in the
(possibly empty) list of \emph{binding clauses}, which indicate the binders
and their scope in a term-constructor. They come in three \emph{modes}:
-
+ %
\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}\\
+ \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}
\end{tabular}
\end{center}
-
+ %
\noindent
The first mode is for binding lists of atoms (the order of binders matters);
the second is for sets of binders (the order does not matter, but the
@@ -1027,17 +1027,17 @@
\begin{equation}\label{letpat}
\mbox{\small%
\begin{tabular}{l}
- \isacommand{nominal\_datatype} @{text trm} =\\
+ \isacommand{nominal\_datatype} @{text trm} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
\hspace{5mm}$\mid$~@{term "App trm trm"}\\
\hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
\;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
\hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
\;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
- \isacommand{and} @{text pat} =\\
- \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
- \hspace{5mm}$\mid$~@{text "PVar name"}\\
- \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
+ \isacommand{and} @{text pat} $=$
+ @{text PNil}
+ $\mid$~@{text "PVar name"}
+ $\mid$~@{text "PTup pat pat"}\\
\isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
\isacommand{where}~@{text "bn(PNil) = []"}\\
\hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
@@ -1070,14 +1070,14 @@
\begin{equation}\label{letrecs}
\mbox{\small%
\begin{tabular}{@ {}l@ {}}
- \isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\
+ \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
\hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
- \isacommand{and} @{text "ass"} =\\
- \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
- \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
+ \isacommand{and} @{text "assn"} $=$
+ @{text "ANil"}
+ $\mid$~@{text "ACons name trm assn"}\\
\isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
\isacommand{where}~@{text "bn(ANil) = []"}\\
\hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
@@ -1197,21 +1197,21 @@
free-atom functions from the specification. For the
\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
%
- \begin{equation}\label{fvars}
- @{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
- \end{equation}
-
- \noindent
+ %\begin{equation}\label{fvars}
+ @{text "fa_ty\<^isub>"}$_{1..n}$
+ %\end{equation}
+ %
+ %\noindent
by recursion.
We define these functions together with auxiliary free-atom functions for
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
we define
%
- \begin{center}
- @{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
- \end{center}
-
- \noindent
+ %\begin{center}
+ @{text "fa_bn\<^isub>"}$_{1..m}$.
+ %\end{center}
+ %
+ %\noindent
The reason for this setup is that in a deep binder not all atoms have to be
bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
that calculates those free atoms in a deep binder.
@@ -1254,8 +1254,9 @@
\noindent
where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
- we are defining by recursion
- (see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+ we are defining by recursion;
+ %(see \eqref{fvars});
+ otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
for atom types to which shallow binders may refer
@@ -1276,8 +1277,8 @@
\noindent
Like the function @{text atom}, the function @{text "atoms"} coerces
- a set of atoms to a set of the generic atom type. It is defined as
- @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+ a set of atoms to a set of the generic atom type.
+ %It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
The set @{text B} is then formally defined as
%
\begin{center}
@@ -1341,7 +1342,7 @@
"fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
"fa\<^bsub>bn\<^esub>"} as follows:
%
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
@{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
@@ -1388,7 +1389,7 @@
"ty"}$_{1..n}$ from the specification. We write them as
%
%\begin{center}
- @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
+ @{text "\<approx>ty"}$_{1..n}$.
%\end{center}
%
%\noindent
@@ -1396,7 +1397,7 @@
define auxiliary $\alpha$-equivalence relations
%
%\begin{center}
- @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
+ @{text "\<approx>bn\<^isub>"}$_{1..m}$
%\end{center}
%
%\noindent
@@ -1406,9 +1407,9 @@
%
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
- @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
- @{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\
+ @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
+ @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
+ @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\
\end{tabular}
\end{center}
@@ -1563,7 +1564,7 @@
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$ with the following clauses:
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}c @ {}}
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
@@ -1572,7 +1573,7 @@
\end{tabular}
\end{center}
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
@@ -1580,7 +1581,7 @@
\end{tabular}
\end{center}
- \begin{center}
+ \begin{center}\small
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
@@ -1615,7 +1616,7 @@
\begin{lemma}\label{equiv}
Given the raw types @{text "ty"}$_{1..n}$ and binding functions
@{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and
- @{text "\<approx>bn"}$_{1..m}$ are equivalence relations and equivariant.
+ @{text "\<approx>bn"}$_{1..m}$ are equivalence relations.%% and equivariant.
\end{lemma}
\begin{proof}
@@ -1721,8 +1722,10 @@
operations defined in \eqref{ceqvt}. In order to make this
lifting to go through, we have to show that the permutation operations are respectful.
This amounts to showing that the
- $\alpha$-equivalence relations are equivariant, which we already established
- in Lemma~\ref{equiv}. As a result we can add the equations
+ $\alpha$-equivalence relations are equivariant \cite{HuffmanUrban10}.
+ %, which we already established
+ %in Lemma~\ref{equiv}.
+ As a result we can add the equations
%
\begin{equation}\label{calphaeqvt}
@{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
@@ -1736,9 +1739,10 @@
The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
by the datatype package of Isabelle/HOL.
- Finally we can add to our infrastructure a structural induction principle
- for the types @{text "ty\<AL>"}$_{i..n}$ whose
- conclusion of the form
+ Finally we can add to our infrastructure a cases lemma (explained in the next section)
+ and a structural induction principle
+ for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
+ of the form
%
\begin{equation}\label{weakinduct}
\mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
@@ -1805,8 +1809,10 @@
for the types @{text "ty\<AL>"}$_{1..n}$
by first lifting definitions from the raw level to the quotient level and
then by establishing facts about these lifted definitions. All necessary proofs
- are generated automatically by custom ML-code. This code can deal with
- specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
+ are generated automatically by custom ML-code.
+
+ %This code can deal with
+ %specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
%\begin{figure}[t!]
%\begin{boxedminipage}{\linewidth}
@@ -2084,17 +2090,17 @@
representations have to resort to the iterated-single-binders-approach with
all the unwanted consequences when reasoning about the resulting terms.
- Two formalisations involving general binders have been
- performed in older
- versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
- \cite{BengtsonParow09,UrbanNipkow09}). Both
- use the approach based on iterated single binders. Our experience with
- the latter formalisation has been disappointing. The major pain arose from
- the need to ``unbind'' variables. This can be done in one step with our
- general binders described in this paper, but needs a cumbersome
- iteration with single binders. The resulting formal reasoning turned out to
- be rather unpleasant. The hope is that the extension presented in this paper
- is a substantial improvement.
+ %Two formalisations involving general binders have been
+ %performed in older
+ %versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
+ %\cite{BengtsonParow09,UrbanNipkow09}). Both
+ %use the approach based on iterated single binders. Our experience with
+ %the latter formalisation has been disappointing. The major pain arose from
+ %the need to ``unbind'' variables. This can be done in one step with our
+ %general binders described in this paper, but needs a cumbersome
+ %iteration with single binders. The resulting formal reasoning turned out to
+ %be rather unpleasant. The hope is that the extension presented in this paper
+ %is a substantial improvement.
The most closely related work to the one presented here is the Ott-tool
\cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
@@ -2119,36 +2125,38 @@
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
+ \isacommand{bind (res)}.
- \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"}\\
- @{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"}\\
- \end{tabular}
- \end{center}
+ %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"}\\
+ %@{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"}\\
+ %\end{tabular}
+ %\end{center}
+ %
+ %\noindent
+ %In the first term-constructor we have a single
+ %body that happens to be ``spread'' over two arguments; in the second term-constructor we have
+ %two independent bodies in which the same variables are bound. As a result we
+ %have
+ %
+ %\begin{center}
+ %\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+ %@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
+ %@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
+ %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
+ %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+ %\end{tabular}
+ %\end{center}
\noindent
- In the first term-constructor we have a single
- body that happens to be ``spread'' over two arguments; in the second term-constructor we have
- two independent bodies in which the same variables are bound. As a result we
- have
-
- \begin{center}
- \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
- @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
- @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
- @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
- @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
- \end{tabular}
- \end{center}
-
- \noindent
- and therefore need the extra generality to be able to distinguish between
- both specifications.
+ %and therefore need the extra generality to be able to distinguish between
+ %both specifications.
Because of how we set up our definitions, we also had to impose some restrictions
(like a single binding function for a deep binder) that are not present in Ott. Our
expectation is that we can still cover many interesting term-calculi from
@@ -2187,10 +2195,11 @@
$\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. We also introduced two binding modes (set and res) that do not
+ 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
+ and a dozen of other calculi from programming language research. The code
will eventually become part of the next Isabelle distribution.\footnote{For the moment
it can be downloaded from the Mercurial repository linked at
\href{http://isabelle.in.tum.de/nominal/download}
@@ -2204,31 +2213,31 @@
definitions to equivariant functions (for such functions it is possible to
provide more automation).
- There are some restrictions we imposed in this paper that we would like to lift in
- future work. One is the exclusion of nested datatype definitions. Nested
- datatype definitions allow one to specify, for instance, the function kinds
- in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
- version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
- achieve this, we need a slightly more clever implementation than we have at the moment.
+ %There are some restrictions we imposed in this paper that we would like to lift in
+ %future work. One is the exclusion of nested datatype definitions. Nested
+ %datatype definitions allow one to specify, for instance, the function kinds
+ %in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
+ %version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
+ %achieve this, we need a slightly more clever implementation than we have at the moment.
- A more interesting line of investigation is whether we can go beyond the
- simple-minded form of binding functions that we adopted from Ott. At the moment, binding
- functions can only return the empty set, a singleton atom set or unions
- of atom sets (similarly for lists). It remains to be seen whether
- properties like
+ %A more interesting line of investigation is whether we can go beyond the
+ %simple-minded form of binding functions that we adopted from Ott. At the moment, binding
+ %functions can only return the empty set, a singleton atom set or unions
+ %of atom sets (similarly for lists). It remains to be seen whether
+ %properties like
+ %%
+ %\begin{center}
+ %@{text "fa_ty x = bn x \<union> fa_bn x"}.
+ %\end{center}
%
- \begin{center}
- @{text "fa_ty x = bn x \<union> fa_bn x"}.
- \end{center}
-
- \noindent
- allow us to support more interesting binding functions.
-
- We have also not yet played with other binding modes. For example we can
- imagine that there is need for a binding mode
- where instead of lists, we abstract lists of distinct elements.
- Once we feel confident about such binding modes, our implementation
- can be easily extended to accommodate them.
+ %\noindent
+ %allow us to support more interesting binding functions.
+ %
+ %We have also not yet played with other binding modes. For example we can
+ %imagine that there is need for a binding mode
+ %where instead of lists, we abstract lists of distinct elements.
+ %Once we feel confident about such binding modes, our implementation
+ %can be easily extended to accommodate them.
\medskip
\noindent