--- a/Paper/Paper.thy Wed Jul 07 13:13:18 2010 +0100
+++ b/Paper/Paper.thy Fri Jul 09 10:00:37 2010 +0100
@@ -623,7 +623,7 @@
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
- atomss; moreover there must be a permutation @{text p} such that {\it
+ atoms; moreover there must be a permutation @{text p} such that {\it
(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@@ -950,7 +950,7 @@
the ones of Ott. The
main idea behind these restrictions is that we obtain a sensible notion of
$\alpha$-equivalence where it is ensured that within a given scope an
- atom occurence cannot be both bound and free at the same time. The first
+ atom occurrence cannot be both bound and free at the same time. The first
restriction is that a body can only occur in
\emph{one} binding clause of a term constructor (this ensures that the bound
atoms of a body cannot be free at the same time by specifying an
@@ -1087,9 +1087,9 @@
\noindent
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
- out different atoms to become bound, respectively be free, in @{text "p"}
- (since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
- such specifications).
+ out different atoms to become bound, respectively be free, in @{text "p"}.
+ (Since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
+ such specifications.)
We also need to restrict the form of the binding functions in order
to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
@@ -1170,9 +1170,9 @@
The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
non-empty and the types in the constructors only occur in positive
- position (see \cite{Berghofer99} for an indepth description of the datatype package
- in Isabelle/HOL). We then define each of the user-specified binding
- function @{term "bn\<^isub>i"} by recursion over the corresponding
+ position (see \cite{Berghofer99} for an in-depth description of the datatype package
+ in Isabelle/HOL). We subsequently define each of the user-specified binding
+ functions @{term "bn"}$_{1..m}$ by recursion over the corresponding
raw datatype. We can also easily define permutation operations by
recursion so that for each term constructor @{text "C"} we have that
%
@@ -1181,7 +1181,7 @@
\end{equation}
The first non-trivial step we have to perform is the generation of
- free-atom functions from the specifications. For the
+ 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}
@@ -1201,7 +1201,7 @@
\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 unbound atoms in a deep binder.
+ that calculates those free atoms in a deep binder.
While the idea behind these free-atom functions is clear (they just
collect all atoms that are not bound), because of our rather complicated
@@ -1209,41 +1209,43 @@
a term-constructor @{text "C"} of type @{text ty} and some associated
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 define below what @{text "fa"} for a binding
+ "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).
Suppose the binding clause @{text bc\<^isub>i} is of the form
%
- \begin{equation}
+ \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{equation}
+ \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
- functions taking a single label as argument (in case of deep binders). Assuming the
- set @{text "D"} stands for the free atoms in the bodies, the set @{text B} for the
- binding atoms in the binders and @{text "B'"} for the free atoms in
+ functions taking a single label as argument (in case of deep binders). Assuming
+ @{text "D"} stands for the set of free atoms of the bodies, @{text B} for the
+ set of binding atoms in the binders and @{text "B'"} for the set of free atoms in
non-recursive deep binders,
- then the free atoms of the binding clause @{text bc\<^isub>i} are given by
+ then the free atoms of the binding clause @{text bc\<^isub>i} are
%
- \begin{center}
- @{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}
- \end{center}
+ \begin{equation}\label{fadef}
+ \mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
+ \end{equation}
\noindent
- whereby the set @{text D} is formally defined as
+ The set @{text D} is formally defined as
%
\begin{center}
@{text "D \<equiv> fa_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fa_ty\<^isub>q d\<^isub>q"}
\end{center}
\noindent
- The functions @{text "fa_ty\<^isub>i"} are the ones we are defining by recursion
- (see \eqref{fvars}) in case the @{text "d\<^isub>i"} refers to one of the raw types
- @{text "ty"}$_{1..n}$ from the specification; otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
- In order to define the set @{text B} we use the following auxiliary @{text "bn"}-functions
- for atom types to which shallow binders have to refer
+ 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"}.
+
+ 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}
@@ -1254,8 +1256,8 @@
\end{center}
\noindent
- The function @{text "atoms"} coerces
- the set of atoms to a set of the generic atom type. It is defined as
+ 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}"}.
The set @{text B} is then formally defined as
%
@@ -1264,28 +1266,30 @@
\end{center}
\noindent
+ where we use the auxiliary binding functions for shallow binders.
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 a\<^isub>1, \<dots>, bn\<^isub>r a\<^isub>r"}
+ @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}
\end{center}
\noindent
- with none of the @{text "a"}$_{1..r}$ being among the bodies @{text
+ with none of the @{text "l"}$_{1..r}$ being among the bodies @{text
"d"}$_{1..q}$. The set @{text "B'"} is defined as
%
\begin{center}
- @{text "B' \<equiv> fa_bn\<^isub>1 a\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r a\<^isub>r"}
+ @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
\end{center}
\noindent
- This completes the definition of the free-atom functions.
+ This completes the definition of the free-atom functions @{text "fa_ty"}$_{1..n}$.
- Note that for non-recursive deep binders, we have to add all atoms that are left
- unbound by the binding function @{text "bn"} (the set @{text "B'"}). We use for this
- the functions @{text "fa_bn"}, also defined by recursion. Assume the user specified
- a @{text bn}-clause of the form
+ Note that for non-recursive deep binders, we have to add in \eqref{fadef}
+ the set of atoms that are left unbound by the binding functions @{text
+ "bn"}$_{1..m}$. We use for the definition of
+ 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}
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
@@ -1298,7 +1302,7 @@
\begin{center}
\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
$\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"}),\\
+ (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"}
with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\\
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
@@ -1307,13 +1311,15 @@
\end{center}
\noindent
- For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these values.
+ For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
- To see how these definitions work in practice, let us reconsider the term-constructors
- @{text "Let"} and @{text "Let_rec"}, as well as @{text "ANil"} and @{text "ACons"}
- from the example shown in \eqref{letrecs}.
- For them we define three free-atom functions, namely
- @{text "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text "fa\<^bsub>bn\<^esub>"} as follows:
+ To see how these definitions work in practice, let us reconsider the
+ term-constructors @{text "Let"} and @{text "Let_rec"} shown in
+ \eqref{letrecs} together with the term-constructors for assignments @{text
+ "ANil"} and @{text "ACons"}. Since there is a binding function defined for
+ assignments, we have three free-atom functions, namely @{text
+ "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
+ "fa\<^bsub>bn\<^esub>"} as follows:
%
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1329,30 +1335,37 @@
\end{center}
\noindent
- To see the pattern, recall that @{text ANil} and @{text "ACons"} have no
+ For these definitions, recall that @{text ANil} and @{text "ACons"} have no
binding clause in the specification. The corresponding free-atom
- function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all atoms
- occurring in an assignment. The binding only takes place in @{text Let} and
- @{text "Let_rec"}. In the @{text "Let"}-clause, the binding clause specifies
+ function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms
+ occurring in an assignment (in case of @{text "ACons"}, they are given by
+ calls to @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}).
+ The binding only takes place in @{text Let} and
+ @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies
that all atoms given by @{text "set (bn as)"} have to be bound in @{text
t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
"fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
- free in @{text "as"}. In contrast, in @{text "Let_rec"} we have a recursive
- binder where we want to also bind all occurrences of the atoms in @{text
+ free in @{text "as"}. This is
+ in contrast with @{text "Let_rec"} where we have a recursive
+ 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 the union @{text "fa\<^bsub>trm\<^esub> t"} and @{text "fa\<^bsub>assn\<^esub> as"}.
-
+ @{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, that means in this
+ example the free atoms in the argument @{text "t"}.
+
An interesting point in this
- example is that a ``naked'' assignment does not bind any
- atoms. Only in the context of a @{text Let} or @{text "Let_rec"} will
- some atoms from an assignment become bound. This is a phenomenon that has also been pointed
+ example is that a ``naked'' assignment (@{text "ANil"} or @{text "ACons"}) does not bind any
+ atoms, even if the binding function is specified over assignments.
+ Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will
+ some atoms actually become bound. This is a phenomenon that has also been pointed
out in \cite{ott-jfp}. For us this observation is crucial, because we would
- not be able to lift the @{text "bn"}-function if it was defined over assignments
- where some atoms are bound. In that case @{text "bn"} would \emph{not} respect
+ not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on
+ atoms that are bound. In that case, these functions would \emph{not} respect
$\alpha$-equivalence.
- Next we define $\alpha$-equivalence relations for the raw types @{text
- "ty"}$_{1..n}$. We write them
+ Next we define the $\alpha$-equivalence relations for the raw types @{text
+ "ty"}$_{1..n}$ from the specification. We write them as
%
\begin{center}
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
@@ -1369,33 +1382,162 @@
\noindent
for the binding functions @{text "bn"}$_{1..m}$,
To simplify our definitions we will use the following abbreviations for
- equivalence relations and free-atom functions acting on pairs
-
+ \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, 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 "(fa\<^isub>1 \<oplus> fa\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x \<union> fa\<^isub>2 y"}\\
+ @{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 "(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}
- The relations for $\alpha$-equivalence are inductively defined
- predicates, whose clauses have the form
+ The $\alpha$-equivalence relations are defined as inductive predicates
+ having a single clause for each term-constructor. Assuming a
+ term-constructor @{text C} is of type @{text ty} and has the binding clauses
+ @{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form
%
\begin{center}
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n \<approx>ty C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
- {@{text "prems(bc\<^isub>1) \<and> \<dots> \<and> prems(bc\<^isub>k)"}}}
+ {@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}}
+ \end{center}
+
+ \noindent
+ The task below is to specify what the premises of a binding clause are. As a
+ special instance, we first treat the case where @{text "bc\<^isub>i"} is the
+ empty binding clause of the form
+ %
+ \begin{center}
+ \mbox{\isacommand{bind\_set} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+ \end{center}
+
+ \noindent
+ In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this
+ we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
+ whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and
+ respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate
+ two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows
+ %
+ \begin{equation}\label{rempty}
+ \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
+ \end{equation}
+
+ \noindent
+ with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding labels @{text "d\<^isub>i"} and
+ @{text "d\<PRIME>\<^isub>i"} refer
+ to a recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
+ we take @{text "R\<^isub>i"} to be the equality @{text "="}. This lets us define
+ 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
+ We will use the unfolded version in the examples below.
+
+ 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"}.}
+ \end{equation}
+
+ \noindent
+ In this case we define a premise @{text P} using the relation
+ $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
+ $\approx_{\,\textit{res}}$ and $\approx_{\,\textit{list}}$ for the other
+ binding modes). This premise defines $\alpha$-equivalence of two abstractions
+ involving multiple binders. We first define as above the tuples @{text "D"} and
+ @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
+ compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}).
+ For $\approx_{\,\textit{set}}$ we also need
+ a compound free-atom function for the bodies defined as
+ %
+ \begin{center}
+ \mbox{@{text "fa \<equiv> (fa_ty\<^isub>1,\<dots>, fa_ty\<^isub>q)"}}
+ \end{center}
+
+ \noindent
+ with assumption that the @{text "d"}$_{1..q}$ refer to arguments of types @{text "ty"}$_{1..q}$.
+ The last ingredient we need are the sets of atoms bound in the bodies.
+ For this we take
+
+ \begin{center}
+ @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> \<dots> \<union> bn_ty\<^isub>p b\<^isub>p"}\;.\\
\end{center}
\noindent
- assuming the term-constructor @{text C} is of type @{text ty} and has
- the binding clauses @{term "bc"}$_{1..k}$. The task
- is to specify what the premises of these clauses are. Again for this we
- analyse the binding clauses and produce a corresponding premise.
+ Similarly for @{text "B'"} using the labels @{text "b\<PRIME>"}$_{1..p}$. This
+ lets us formally define the premise @{text P} for a non-empty binding clause as:
+ %
+ \begin{equation}\label{pprem}
+ \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+ \end{equation}
+
+ \noindent
+ This premise accounts for $\alpha$-equivalence of the bodies of the binding
+ clause. However, in case the binders have non-recursive deep binders, then
+ we also have to ``propagate'' $\alpha$-equivalence inside the structure of
+ these binders. An example is @{text "Let"} where we have to make sure the
+ right-hand sides of assignments are $\alpha$-equivalent. For this we use the
+ 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}
+ @{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}.
+ \end{center}
+
+ \noindent
+ The premises for @{text "bc\<^isub>i"} are then defined as
+ %
+ \begin{center}
+ @{text "prems(bc\<^isub>i) \<equiv> P \<and> l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1 \<and> ... \<and> l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
+ \end{center}
+
+ \noindent
+ where @{text "P"} is defined in \eqref{pprem}.
+
+ The $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$ are defined as follows:
+ given a @{text bn}-clause of the form
+ %
+ \begin{center}
+ @{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
+ \end{center}
+
+ \noindent
+ where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
+ then the $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+ %
+ \begin{center}
+ \mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
+ {@{text "z\<^isub>1 R\<^isub>1 z\<PRIME>\<^isub>1 \<dots> z\<^isub>s R\<^isub>s z\<PRIME>\<^isub>s"}}}
+ \end{center}
+
+ \noindent
+ whereby the relations @{text "R"}$_{1..s}$ are given by
+
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ $\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}
+ and is a non-recursive argument of @{text C},\\
+ $\bullet$ & @{text "z\<^isub>i \<approx>bn\<^isub>i z\<PRIME>\<^isub>i"} provided @{text "z\<^isub>i"} occurs in @{text rhs}
+ with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\\
+ $\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
+ recursive call.
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
+ that the premises of empty binding clauses are a special case of the clauses for
+ non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
+ as the permutation).
*}
-(*<*)
-consts alpha_ty ::'a
+(*<*)consts alpha_ty ::'a
consts alpha_trm ::'a
consts fa_trm :: 'a
consts alpha_trm2 ::'a
@@ -1405,77 +1547,16 @@
alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
fa_trm ("fa\<^bsub>trm\<^esub>") and
alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
- fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")
-(*>*)
+ fa_trm2 ("fa\<^bsub>assn\<^esub> \<oplus> fa\<^bsub>trm\<^esub>")(*>*)
text {*
- *TBD below *
-
- \begin{equation}\label{alpha}
- \mbox{%
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- \multicolumn{2}{@ {}l}{Empty binding clauses of the form
- \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\
- $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"}
- are recursive arguments of @{text "C"}\\
- $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are
- non-recursive arguments\smallskip\\
- \multicolumn{2}{@ {}l}{Shallow binders of the form
- \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
- $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
- @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
- @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then
- \begin{center}
- @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
- \end{center}\\
- \multicolumn{2}{@ {}l}{Deep binders of the form
- \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\
- $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},
- @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fa} is
- @{text "fa_ty\<^isub>1 \<oplus> ... \<oplus> fa_ty\<^isub>m"}, then for recursive deep binders
- \begin{center}
- @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fa p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}
- \end{center}\\
- $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\
- \end{tabular}}
- \end{equation}
-
- \noindent
- Similarly for the other binding modes.
- From this definition it is clear why we have to impose the restriction
- of excluding overlapping deep binders, as these would need to be translated into separate
- abstractions.
-
-
-
- The $\alpha$-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions
- are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
- and need to generate appropriate premises. We generate first premises according to the first three
- rules given above. Only the ``left-over'' pairs @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated
- differently. They depend on whether @{text "x\<^isub>i"} occurs in @{text "rhs"} of the
- clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
-
- \begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
- and the type of @{text "x\<^isub>i"} is @{text ty} and @{text "x\<^isub>i"} is a recursive argument
- in the term-constructor\\
- $\bullet$ & @{text "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
- and @{text "x\<^isub>i"} is not a recursive argument in the term-constructor\\
- $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}
- with the recursive call @{text "bn x\<^isub>i"}\\
- $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
- in a recursive call involving a @{text "bn"}
- \end{tabular}
- \end{center}
-
Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
- we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
- $\approx_{\textit{bn}}$, with the clauses as follows:
+ we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
+ $\approx_{\textit{bn}}$ with the following clauses:
\begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
- {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"}}\smallskip\\
+ {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
{@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fa_trm2 p (bn as', (as', t'))"}}
\end{tabular}