--- a/Paper/Paper.thy Wed Mar 31 18:47:22 2010 +0200
+++ b/Paper/Paper.thy Wed Mar 31 22:48:35 2010 +0200
@@ -578,11 +578,10 @@
fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
@{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
- All properties given in this section are formalised in Isabelle/HOL and
- most of proofs are described in \cite{HuffmanUrban10} to which we refer the
- reader. In the next sections we will make extensively use of these
- properties in order to define alpha-equivalence in the presence of multiple
- binders.
+ Most properties given in this section are described in \cite{HuffmanUrban10}
+ and of course all are formalised in Isabelle/HOL. In the next sections we will make
+ extensively use of these properties in order to define alpha-equivalence in
+ the presence of multiple binders.
*}
@@ -767,8 +766,8 @@
\noindent
indicating that a set (or list) @{text as} is abstracted in @{text x}. We will
call the types \emph{abstraction types} and their elements
- \emph{abstractions}. The important property we need to derive is what the
- support of abstractions is, namely:
+ \emph{abstractions}. The important property we need to derive the support of
+ abstractions, namely:
\begin{thm}[Support of Abstractions]\label{suppabs}
Assuming @{text x} has finite support, then\\[-6mm]
@@ -825,7 +824,7 @@
which by Property~\ref{supportsprop} gives us ``one half'' of
Thm~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
it, we use a trick from \cite{Pitts04} and first define an auxiliary
- function taking an abstraction as argument:
+ function @{text aux}, taking an abstraction as argument:
%
\begin{center}
@{thm supp_gen.simps[THEN eq_reflection, no_vars]}
@@ -850,15 +849,17 @@
\end{equation}
\noindent
- since for finite sets, @{text "S"}, we have @{thm (concl) supp_finite_atom_set[no_vars]}.
+ since for finite sets of atoms, @{text "bs"}, we have
+ @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+ Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
+ Theorem~\ref{suppabs}.
- Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes of
- Theorem~\ref{suppabs}. The method of first considering abstractions of the
+ The method of first considering abstractions of the
form @{term "Abs as x"} etc is motivated by the fact that properties about them
can be conveninetly established at the Isabelle/HOL level. It would be
difficult 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 also help us in the next section.
+ the definitions for alpha-equivalence will help us in the next section.
*}
section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -906,12 +907,15 @@
\end{center}
\noindent
- whereby some of the @{text ty}$'_{1..l}$ (or their components) are contained
+ whereby some of the @{text ty}$'_{1..l}$ (or their components) might 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
- \emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. There are ``positivity''
- restrictions imposed in the type of such recursive arguments, which ensure
- that the type has a set-theoretic semantics \cite{Berghofer99}. The labels
+ \eqref{scheme}.
+ %In this case we will call the corresponding argument a
+ %\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such recursive
+ %arguments need to satisfy a ``positivity''
+ %restriction, which ensures that the type has a set-theoretic semantics
+ %\cite{Berghofer99}.
+ The labels
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}:
@@ -929,8 +933,8 @@
the second is for sets of binders (the order does not matter, but the
cardinality does) and the last is for sets of binders (with vacuous binders
preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
- clause will be called the \emph{body} of the abstraction; the
- ``\isacommand{bind}-part'' will be the \emph{binder} of the binding clause.
+ clause will be called the \emph{body}; the
+ ``\isacommand{bind}-part'' will be the \emph{binder}.
In addition we distinguish between \emph{shallow} and \emph{deep}
binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\;
@@ -986,7 +990,7 @@
(for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms
(for \isacommand{bind}). They can be defined by primitive 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 lets
+ the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s
with tuple patterns might be specified as:
\begin{center}
@@ -1066,7 +1070,8 @@
Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
Whenever such a binding clause is present, we will call the binder \emph{recursive}.
- To see the purpose for such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s:
+ To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s
+ in the following specification:
%
\begin{equation}\label{letrecs}
\mbox{%
@@ -1161,7 +1166,7 @@
\noindent
The reason for this setup is that in a deep binder not all atoms have to be
bound, as we shall see in an example below. We need therefore the function
- that returns us those unbound atoms.
+ that calculates those unbound atoms.
While the idea behind these
free-variable functions is clear (they just collect all atoms that are not bound),
@@ -1170,7 +1175,7 @@
Given a term-constructor @{text "C"} of type @{text ty} with argument types
\mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
@{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
- calculated next for each argument.
+ calculated below for each argument.
First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses,
we can determine whether the argument is a shallow or deep
binder, and in the latter case also whether it is a recursive or
@@ -1201,8 +1206,8 @@
either the corresponding binders are all shallow or there is a single deep binder.
In the former case we take @{text bnds} to be the union of all shallow
binders; in the latter case, we just take the set of atoms specified by the
- binding function. The value for @{text "x\<^isub>i"} is then given by:
-
+ corrsponding binding function. The value for @{text "x\<^isub>i"} is then given by:
+ %
\begin{equation}\label{deepbody}
\mbox{%
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
@@ -1218,9 +1223,9 @@
\end{equation}
\noindent
- Like the coercion function @{text atom} used above, @{text "atoms as"} coerces
+ Like the coercion function @{text atom} used earlier, @{text "atoms as"} coerces
the set @{text as} to the generic atom type.
- It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.
+ It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
The last case we need to consider is when @{text "x\<^isub>i"} is neither
a binder nor a body of an abstraction. In this case it is defined
@@ -1228,12 +1233,12 @@
set @{text bnds}.
Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for
- each binding function @{text "bn\<^isub>j"}. The idea behind this
- function is to compute the set of free atoms that are not bound by
+ each binding function @{text "bn\<^isub>j"}. The idea behind these
+ functions is to compute the set of free atoms that are not bound by
@{text "bn\<^isub>j"}. Because of the restrictions we imposed on the
form of binding functions, this can be done automatically by recursively
building up the the set of free variables from the arguments that are
- not bound. Let us assume one clause of the binding function is
+ not bound. Let us assume one clause of a binding function is
@{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j"} is the
union of the values calculated for @{text "x\<^isub>i"} of type @{text "ty\<^isub>i"}
as follows:
@@ -1245,7 +1250,11 @@
atom list or atom set\\
$\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the
recursive call @{text "bn x\<^isub>i"}\medskip\\
- %
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
\multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
$\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\
$\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
@@ -1260,8 +1269,8 @@
\noindent
To see how these definitions work in practise, let us reconsider the term-constructors
- @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}.
- For this specification we need to define three functions, namely
+ @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}.
+ For this specification we need to define three free-variable functions, namely
@{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
%
\begin{center}
@@ -1293,10 +1302,10 @@
"set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
@{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
that an assignment ``alone'' does not have any bound variables. Only in the
- context of a @{text Let} or @{text "Let_rec"} will some atoms become bound
- (the term-constructors that have binding clauses). This is a phenomenon
+ context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
+ This is a phenomenon
that has also been pointed out in \cite{ott-jfp}. We can also see that
- given a @{text "bn"}-function for a type @{text "ty"}, then we have
+ given a @{text "bn"}-function for a type @{text "ty"}, we have that
%
\begin{equation}\label{bnprop}
@{text "fv_ty x = bn x \<union> fv_bn x"}.
@@ -1305,12 +1314,12 @@
Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions,
we also need to define auxiliary alpha-equivalence relations for the binding functions.
- Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.
+ Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}.
To simplify our definitions we will use the following abbreviations for
relations and free-variable acting on products.
%
\begin{center}
- \begin{tabular}{rcl}
+ \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\
@{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\
\end{tabular}
@@ -1318,11 +1327,19 @@
The relations for alpha-equivalence are inductively defined predicates, whose clauses have
- conclusions of the form @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} (let us assume
+ conclusions of the form
+ %
+ \begin{center}
+ @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+ \end{center}
+
+ \noindent
+ For what follows, let us assume
@{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).
The task now is to specify what the premises of these clauses are. For this we
- consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"}. We will analyse these pairs according to
- ``clusters'' of the binding clauses. There are the following cases:
+ consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will
+ be easier to analyse these pairs according to ``clusters'' of the binding clauses.
+ Therefore we distinguish the following cases:
*}
(*<*)
consts alpha_ty ::'a
@@ -1331,33 +1348,34 @@
text {*
\begin{itemize}
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the
- @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding binders. For the binding mode
+ \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
\isacommand{bind\_set} we generate the premise
\begin{center}
@{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty\<^isub>i p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
\end{center}
- Similarly for the other modes.
+ For the binding mode \isacommand{bind} we use $\approx_{\textit{list}}$, and for
+ binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$.
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}
- and with @{text bn} being the auxiliary binding function. We assume
+ and @{text bn} being the auxiliary binding function. We assume
@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
- For the binding mode \isacommand{bind\_set} we generate the two premises
-
+ For the binding mode \isacommand{bind\_set} we generate two premises
+ %
\begin{center}
- @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\\
+ @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\hfill
@{term "\<exists>p. (bn x\<^isub>i, (u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (v\<^isub>1,\<xi>,v\<^isub>m))"}
\end{center}
\noindent
where @{text R} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
- @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.
+ @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.
\item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep recursive binders with type @{text "ty"}
and with @{text bn} being the auxiliary binding function. We assume
@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
For the binding mode \isacommand{bind\_set} we generate the premise
-
+ %
\begin{center}
@{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}
\end{center}
@@ -1368,11 +1386,18 @@
\end{itemize}
\noindent
- The only cases that are not covered by these rules is if @{text "(x\<^isub>i, y\<^isub>i)"} is
+ From these definition it is clear why we can only support one binding mode per binder
+ and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$
+ and $\approx_{\textit{res}}$. It is also clear why we had to impose the restriction
+ of excluding overlapping binders, as these would need to be translated to separate
+ abstractions.
+
+
+ The only cases that are not covered by the rules above are the cases where @{text "(x\<^isub>i, y\<^isub>i)"} is
neither a binder nor a body. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided
the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are
- recursive arguments of the term constructor. If they are non-recursive arguments
- then we generate @{text "x\<^isub>i = y\<^isub>i"}.
+ recursive arguments of the term-constructor. If they are non-recursive arguments
+ then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
TODO