--- a/Paper/Paper.thy Tue Oct 05 07:30:37 2010 +0100
+++ b/Paper/Paper.thy Tue Oct 05 08:43:49 2010 +0100
@@ -287,15 +287,15 @@
\draw (-2.0, 0.845) -- (0.7,0.845);
\draw (-2.0,-0.045) -- (0.7,-0.045);
- \draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
- \draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+ \draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
+ \draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
\draw (1.8, 0.48) node[right=-0.1mm]
- {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
- \draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
- \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+ {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+ \draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+ \draw (-3.25, 0.55) node {\footnotesize\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};
+ \draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};
\end{tikzpicture}
\end{center}
@@ -353,15 +353,15 @@
of theorems to the quotient level needs proofs of some respectfulness
properties (see \cite{Homeier05}). In the paper we show that we are able to
automate these proofs and as a result can automatically establish a reasoning
- infrastructure for $\alpha$-equated terms.
+ infrastructure for $\alpha$-equated terms.\smallskip
- The examples we have in mind where our reasoning infrastructure will be
- helpful includes the term language of Core-Haskell. This term language
- involves patterns that have lists of type-, coercion- and term-variables,
- all of which are bound in @{text "\<CASE>"}-expressions. In these
- patterns we do not know in advance how many variables need to
- be bound. Another example is the specification of SML, which includes
- includes bindings as in type-schemes.\medskip
+ %The examples we have in mind where our reasoning infrastructure will be
+ %helpful includes the term language of Core-Haskell. This term language
+ %involves patterns that have lists of type-, coercion- and term-variables,
+ %all of which are bound in @{text "\<CASE>"}-expressions. In these
+ %patterns we do not know in advance how many variables need to
+ %be bound. Another example is the specification of SML, which includes
+ %includes bindings as in type-schemes.\medskip
\noindent
{\bf Contributions:} We provide three new definitions for when terms
@@ -436,7 +436,8 @@
b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for
permutations. The purpose of atoms is to represent variables, be they bound or free.
The sorts of atoms can be used to represent different kinds of
- variables, such as the term-, coercion- and type-variables in Core-Haskell.
+ variables.
+ %%, such as the term-, coercion- and type-variables in Core-Haskell.
It is assumed that there is an infinite supply of atoms for each
sort. However, in the interest of brevity, we shall restrict ourselves
in what follows to only one sort of atoms.
@@ -680,8 +681,8 @@
and @{text bs} are lists of atoms).
If we do not want to make any difference between the order of binders \emph{and}
- also allow vacuous binders, then we keep sets of binders, but drop the fourth
- condition in \eqref{alphaset}:
+ also allow vacuous binders, that means \emph{restrict} names, then we keep sets of binders, but drop
+ condition {\it (iv)} in \eqref{alphaset}:
%
\begin{equation}\label{alphares}
\begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
@@ -780,8 +781,8 @@
\end{theorem}
\noindent
- This theorem states that the bound names do not appear in the support, as expected.
- For brevity we omit the proof of this resul and again refer the reader to
+ This theorem states that the bound names do not appear in the support.
+ For brevity we omit the proof and again refer the reader to
our formalisation in Isabelle/HOL.
%\noindent
@@ -861,7 +862,7 @@
properties about them. It would be
laborious to write custom ML-code that derives automatically such properties
for every term-constructor that binds some atoms. Also the generality of
- the definitions for $\alpha$-equivalence will help us in the next section.
+ the definitions for $\alpha$-equivalence will help us in the next sections.
*}
section {* Specifying General Bindings\label{sec:spec} *}
@@ -882,7 +883,7 @@
\mbox{\begin{tabular}{l}
\isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
\isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
- $\ldots$\\
+ \raisebox{2mm}{$\ldots$}\\[-2mm]
\isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
\end{tabular}}
\end{cases}$\\
@@ -891,7 +892,7 @@
\mbox{\begin{tabular}{l}
\isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
\isacommand{where}\\
- $\ldots$\\
+ \raisebox{2mm}{$\ldots$}\\[-2mm]
\end{tabular}}
\end{cases}$\\
\end{tabular}}
@@ -908,7 +909,8 @@
\end{center}
\noindent
- whereby some of the @{text ty}$'_{1..l}$ (or their components) can be contained
+ whereby some of the @{text ty}$'_{1..l}$ %%(or their components)
+ can be contained
in the collection of @{text ty}$^\alpha_{1..n}$ declared in
\eqref{scheme}.
In this case we will call the corresponding argument a
@@ -937,21 +939,23 @@
preserving $\alpha$-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
clause will be called \emph{bodies}; the
``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
- Ott, we allow multiple labels in binders and bodies. For example we allow
- binding clauses of the form:
+ Ott, we allow multiple labels in binders and bodies.
- \begin{center}
- \begin{tabular}{@ {}ll@ {}}
- @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
- \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
- @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
- \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
- \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
- \end{tabular}
- \end{center}
+ %For example we allow
+ %binding clauses of the form:
+ %
+ %\begin{center}
+ %\begin{tabular}{@ {}ll@ {}}
+ %@{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
+ % \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
+ %@{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
+ % \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
+ % \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
+ %\end{tabular}
+ %\end{center}
\noindent
- Similarly for the other binding modes.
+ %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
%of the specifications (the corresponding $\alpha$-equivalence will differ). We will
@@ -983,14 +987,14 @@
\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
\hspace{5mm}$\mid$~@{text "App lam lam"}\\
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
- \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
+ \hspace{24mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
\isacommand{nominal\_datatype}~@{text ty} $=$\\
\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{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
+ \hspace{29mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
\end{tabular}
\end{tabular}
\end{center}
@@ -1061,8 +1065,7 @@
\begin{equation}\label{letrecs}
\mbox{%
\begin{tabular}{@ {}l@ {}}
- \isacommand{nominal\_datatype}~@{text "trm ="}\\
- \hspace{5mm}\phantom{$\mid$}\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"}
@@ -1111,7 +1114,7 @@
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
may have a binding clause involving the argument @{text t} (the only one that
is \emph{not} used in the definition of the binding function). This restriction
- is sufficient for having the binding function over $\alpha$-equated terms.
+ is sufficient for lifting the binding function to $\alpha$-equated terms.
In the version of
Nominal Isabelle described here, we also adopted the restriction from the
@@ -1127,7 +1130,7 @@
for every argument of a term-constructor that is \emph{not}
already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
- of the lambda-calculus, the completion produces
+ of the lambda-terms, the completion produces
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
@@ -1167,8 +1170,8 @@
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
- that a notion is defined over $\alpha$-equivalence classes and leave it out
- for the corresponding notion defined on the ``raw'' level. So for example
+ that a notion is given for $\alpha$-equivalence classes and leave it out
+ for the corresponding notion given on the ``raw'' level. So for example
we have
\begin{center}
@@ -1224,11 +1227,11 @@
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}
+ %\begin{center}
\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
+ %\end{center}
+ %
+ %\noindent
in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
and the binders @{text b}$_{1..p}$
either refer to labels of atom types (in case of shallow binders) or to binding
@@ -1258,12 +1261,18 @@
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
%
+ %\begin{center}
+ %\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ %@{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+ %@{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+ %@{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
+ %\end{tabular}
+ %\end{center}
+ %
\begin{center}
- \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "bn_atom a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
- @{text "bn_atom_set as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
- @{text "bn_atom_list as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
- \end{tabular}
+ @{text "bn_atom a \<equiv> {atom a}"}\hspace{17mm}
+ @{text "bn_atom_set as \<equiv> atoms as"}\\
+ @{text "bn_atom_list as \<equiv> atoms (set as)"}
\end{center}
\noindent
@@ -1281,11 +1290,11 @@
The set @{text "B'"} collects all free atoms in non-recursive deep
binders. Let us assume these binders in @{text "bc\<^isub>i"} are
%
- \begin{center}
- @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
- \end{center}
-
- \noindent
+ %\begin{center}
+ \mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
+ %\end{center}
+ %
+ %\noindent
with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ and none of the
@{text "l"}$_{1..r}$ being among the bodies @{text
"d"}$_{1..q}$. The set @{text "B'"} is defined as
@@ -1303,16 +1312,16 @@
this set the functions @{text "fa_bn"}$_{1..m}$, which are also defined by mutual
recursion. Assume the user specified a @{text bn}-clause of the form
%
- \begin{center}
+ %\begin{center}
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
- \end{center}
-
- \noindent
+ %\end{center}
+ %
+ %\noindent
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$. For each of
the arguments we calculate the free atoms as follows:
%
\begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
$\bullet$ & @{term "fa_ty\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text "rhs"}
(that means nothing is bound in @{text "z\<^isub>i"} by the binding function),\\
$\bullet$ & @{term "fa_bn\<^isub>i z\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"}
@@ -1321,7 +1330,7 @@
but without a recursive call.
\end{tabular}
\end{center}
-
+ %
\noindent
For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
@@ -1362,9 +1371,9 @@
binder to bind all occurrences of the atoms in @{text
"set (bn as)"} also inside @{text "as"}. Therefore we have to subtract
@{text "set (bn as)"} from both @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
- Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
- list of assignments, but instead returns the free atoms, which means in this
- example the free atoms in the argument @{text "t"}.
+ %Like the function @{text "bn"}, the function @{text "fa\<^bsub>bn\<^esub>"} traverses the
+ %list of assignments, but instead returns the free atoms, which means in this
+ %example the free atoms in the argument @{text "t"}.
An interesting point in this
example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any
@@ -1379,27 +1388,27 @@
Next we define the $\alpha$-equivalence relations for the raw types @{text
"ty"}$_{1..n}$ from the specification. We write them as
%
- \begin{center}
+ %\begin{center}
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
- \end{center}
-
- \noindent
+ %\end{center}
+ %
+ %\noindent
Like with the free-atom functions, we also need to
define auxiliary $\alpha$-equivalence relations
%
- \begin{center}
+ %\begin{center}
@{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
- \end{center}
-
- \noindent
+ %\end{center}
+ %
+ %\noindent
for the binding functions @{text "bn"}$_{1..m}$,
To simplify our definitions we will use the following abbreviations for
\emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
%
\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>"} & \\
- \multicolumn{3}{r}{@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}}\\
+ @{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"}\\
\end{tabular}
\end{center}
@@ -1443,11 +1452,11 @@
the premise for an empty binding clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"},
which can be unfolded to the series of premises
%
- \begin{center}
- @{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1 \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}
- \end{center}
-
- \noindent
+ %\begin{center}
+ @{text "d\<^isub>1 R\<^isub>1 d\<PRIME>\<^isub>1 \<dots> d\<^isub>q R\<^isub>q d\<PRIME>\<^isub>q"}.
+ %\end{center}
+ %
+ %\noindent
We will use the unfolded version in the examples below.
Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form
@@ -1499,11 +1508,11 @@
relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
%
- \begin{center}
+ %\begin{center}
@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
- \end{center}
-
- \noindent
+ %\end{center}
+ %
+ %\noindent
The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.
All premises for @{text "bc\<^isub>i"} are then given by
@@ -1516,11 +1525,11 @@
The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
%
- \begin{center}
+ %\begin{center}
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
- \end{center}
-
- \noindent
+ %\end{center}
+ %
+ %\noindent
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
%
@@ -1533,7 +1542,7 @@
In this clause the relations @{text "R"}$_{1..s}$ are given by
\begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
$\bullet$ & @{text "z\<^isub>i \<approx>ty z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs} and
is a recursive argument of @{text C},\\
$\bullet$ & @{text "z\<^isub>i = z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} does not occur in @{text rhs}
@@ -1566,7 +1575,7 @@
\begin{center}
\begin{tabular}{@ {}c @ {}}
- \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\
+ \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
{@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
\end{tabular}
@@ -1574,7 +1583,7 @@
\begin{center}
\begin{tabular}{@ {}c @ {}}
- \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\smallskip\\
+ \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
{@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
\end{tabular}
@@ -1585,9 +1594,10 @@
$\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of
the components in an assignment that are \emph{not} bound. This is needed in the
in the clause for @{text "Let"} (which is has
- a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant
- to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
- because there all components of an assignment are ``under'' the binder.
+ a non-recursive binder).
+ %The underlying reason is that the terms inside an assignment are not meant
+ %to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
+ %because there all components of an assignment are ``under'' the binder.
*}
section {* Establishing the Reasoning Infrastructure *}