--- a/LMCS-Paper/Paper.thy Fri Sep 09 11:52:24 2011 +0100
+++ b/LMCS-Paper/Paper.thy Fri Sep 09 17:11:38 2011 +0100
@@ -15,6 +15,17 @@
definition
"equal \<equiv> (op =)"
+fun alpha_set_ex where
+ "alpha_set_ex (bs, x) R f (cs, y) = (\<exists>pi. alpha_set (bs, x) R f pi (cs, y))"
+
+fun alpha_res_ex where
+ "alpha_res_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_res (bs, x) R f pi (cs, y))"
+
+fun alpha_lst_ex where
+ "alpha_lst_ex (bs, x) R f pi (cs, y) = (\<exists>pi. alpha_lst (bs, x) R f pi (cs, y))"
+
+
+
notation (latex output)
swap ("'(_ _')" [1000, 1000] 1000) and
fresh ("_ # _" [51, 51] 50) and
@@ -22,9 +33,9 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
- alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_set_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _\<^esup> _") and
+ alpha_lst_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _\<^esup> _") and
+ alpha_res_ex ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set+}}$}}>\<^bsup>_, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and
fv ("fa'(_')" [100] 100) and
@@ -657,7 +668,8 @@
\begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
- @{term "(as, x) \<approx>set R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+ @{term "alpha_set_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+ \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\
& \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\
& \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
& \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"} \\
@@ -666,9 +678,7 @@
\end{defi}
\noindent
- Note that this relation depends on the permutation @{text
- "\<pi>"}; alpha-equivalence between two pairs is then the relation where we
- existentially quantify over this @{text "\<pi>"}. Also note that the relation is
+ Note that the relation is
dependent on a free-atom function @{text "fa"} and a relation @{text
"R"}. The reason for this extra generality is that we will use
$\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
@@ -682,7 +692,8 @@
\begin{defi}[Alpha-Equivalence for List-Bindings]\label{alphalist}\mbox{}\\
\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
- @{term "(as, x) \<approx>lst R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+ @{term "alpha_lst_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+ \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\
& \mbox{\it (i)} & @{term "fa(x) - (set as) = fa(y) - (set bs)"}\\
& \mbox{\it (ii)} & @{term "(fa(x) - set as) \<sharp>* \<pi>"}\\
& \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
@@ -701,7 +712,8 @@
\begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\
\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
- @{term "(as, x) \<approx>res R fa \<pi> (bs, y)"}\hspace{2mm}@{text "\<equiv>"}
+ @{term "alpha_res_ex (as, x) R fa (bs, y)"}\hspace{2mm}@{text "\<equiv>"} &
+ \multicolumn{2}{@ {}l}{if there exists a @{text "\<pi>"} such that:}\\
& \mbox{\it (i)} & @{term "fa(x) - as = fa(y) - bs"}\\
& \mbox{\it (ii)} & @{term "(fa(x) - as) \<sharp>* \<pi>"}\\
& \mbox{\it (iii)} & @{text "(\<pi> \<bullet> x) R y"}\\
@@ -737,24 +749,25 @@
shown that all three notions of alpha-equivalence coincide, if we only
abstract a single atom.
- In the rest of this section we are going to introduce three abstraction
- types. For this we define the relations
+ In the rest of this section we are going to show that the alpha-equivalences really
+ lead to abstractions where some atoms are bound. For this we are going to introduce
+ three abstraction types that are quotients with respect to the relations
\begin{equation}
\begin{array}{r}
- @{term "alpha_abs_set (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}\\
- @{term "alpha_abs_res (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_res (as, x) equal supp \<pi> (bs, y)"}\\
- @{term "alpha_abs_lst (as, x) (bs, y) \<equiv> \<exists>\<pi>. alpha_lst (as, x) equal supp \<pi> (bs, y)"}\\
+ @{term "alpha_abs_set (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_set_ex (as, x) equal supp (bs, y)"}\\
+ @{term "alpha_abs_res (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_res_ex (as, x) equal supp (bs, y)"}\\
+ @{term "alpha_abs_lst (as, x) (bs, y)"}~~@{text "\<equiv>"}~~@{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\
\end{array}
\end{equation}\smallskip
\noindent
- We can show that these relations are equivalence
- relations and equivariant.
+ In these relation we replaced the free-atom function @{text "fa"} with @{term "supp"} and the
+ relation @{text R} with equality. We can show the following properties:
\begin{lem}\label{alphaeq}
- The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
- and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant.
+ The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_set+}}$
+ and $\approx_{\,\textit{abs\_list}}$ are equivalence relations and equivariant.
\end{lem}
\begin{proof}
@@ -763,10 +776,10 @@
of transitivity, we have two permutations @{text "\<pi>\<^isub>1"} and @{text "\<pi>\<^isub>2"}, and for the
proof obligation use @{text "\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means
@{term "abs_set (\<pi> \<bullet> as, \<pi> \<bullet> x) (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided
- @{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the
+ \mbox{@{term "abs_set (as, x) (bs, y)"}} holds. To show this, we need to unfold the
definitions and `pull out' the permutations, which is possible since all
operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant
- (see \cite{HuffmanUrban10}).
+ (see \cite{HuffmanUrban10}). Finally we apply the permutation operation on booleans.
\end{proof}
\noindent
@@ -803,15 +816,17 @@
\end{thm}
\noindent
- In effect, this theorem states that the bound names do not appear in the support
- of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist}
- and \ref{alphares} capture the idea of alpha-equivalence relations.
- Below we will show the first equation of Theorem \ref{suppabs}. The others follow by similar
- arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have
+ In effect, this theorem states that the atoms @{text "as"} are bound in the
+ abstraction. As stated earlier, this can be seen as test that our
+ Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the
+ idea of alpha-equivalence relations. Below we will give the proof for the
+ first equation of Theorem \ref{suppabs}. The others follow by similar
+ arguments. By definition of the abstraction type @{text
+ "abs\<^bsub>set\<^esub>"} we have
\begin{equation}\label{abseqiff}
@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\;
- @{term "\<exists>\<pi>. alpha_set (as, x) equal supp \<pi> (bs, y)"}
+ @{term "alpha_set_ex (as, x) equal supp (bs, y)"}
\end{equation}\smallskip
\noindent
@@ -836,6 +851,7 @@
\begin{proof}
This lemma is straightforward using \eqref{abseqiff} and observing that
the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+ We therefore can use as permutation the swapping @{term "(a \<rightleftharpoons> b)"}.
\end{proof}
\noindent
@@ -867,7 +883,7 @@
\]\smallskip
\noindent
- using fact about function applications in \eqref{supps}. Assuming
+ using the fact about the support of function applications in \eqref{supps}. Assuming
@{term "supp x - as"} is a finite set, we further obtain
\begin{equation}\label{halftwo}
@@ -875,7 +891,7 @@
\end{equation}\smallskip
\noindent
- since for every finite sets of atoms, say @{text "bs"}, we have
+ This is because for every finite sets of atoms, say @{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}.
@@ -898,7 +914,7 @@
collection of (possibly mutual recursive) type declarations, say @{text
"ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
- syntax in Nominal Isabelle for such specifications is roughly as follows:
+ syntax in Nominal Isabelle for such specifications is schematically as follows:
\begin{equation}\label{scheme}
\mbox{\begin{tabular}{@ {}p{2.5cm}l}
@@ -910,7 +926,7 @@
\raisebox{2mm}{$\ldots$}\\[-2mm]
\isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
\end{tabular}}
- \end{cases}$\\
+ \end{cases}$\\[2mm]
binding \mbox{function part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
@@ -986,9 +1002,17 @@
that we obtain a sensible notion of alpha-equivalence where it is ensured
that within a given scope an 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 alternative
- binder for the same body).
+ \emph{one} binding clause of a term constructor. So for example
+
+ \[\mbox{
+ @{text "Foo x::name y::name t::trm"}\hspace{3mm}
+ \isacommand{binds} @{text "x"} \isacommand{in} @{text "t"},
+ \isacommand{binds} @{text "y"} \isacommand{in} @{text "t"}}
+ \]\smallskip
+
+ \noindent
+ is not allowed. This ensures that the bound atoms of a body cannot be free
+ at the same time by specifying an 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
@@ -1021,9 +1045,9 @@
\noindent
In these specifications @{text "name"} refers to an atom type, and @{text
- "fset"} to the type of finite sets. Note that for @{text lam} it does not
+ "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{binds (set)} or \isacommand{binds}
+ @{text name}. However, having \isacommand{binds (set)} or just \isacommand{binds}
in the second case makes a difference to the semantics of the specification
(which we will define in the next section).
@@ -1108,16 +1132,16 @@
To make sure that atoms bound by deep binders cannot be free at the
same time, we cannot have more than one binding function for a deep binder.
Consequently we exclude specifications such as
- %
- \begin{center}
+
+ \[\mbox{
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Baz\<^isub>1 p::pat t::trm"} &
\isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
@{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
\isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
\isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
\noindent
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
@@ -1125,24 +1149,45 @@
(Since the Ott-tool does not derive a reasoning infrastructure for
alpha-equated terms with deep binders, 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
- terms. The main restriction is that we cannot return an atom in a binding function that is also
- bound in the corresponding term-constructor. That means in \eqref{letpat}
- that the term-constructors @{text PVar} and @{text PTup} may
- not have a binding clause (all arguments are used to define @{text "bn"}).
- In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
- may have a binding clause involving the argument @{text trm} (the only one that
- is \emph{not} used in the definition of the binding function). This restriction
- is sufficient for lifting the binding function to alpha-equated terms.
+ 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
+ terms. The main restriction is that we cannot return an atom in a binding
+ function that is also bound in the corresponding term-constructor.
+ Consider again the specification for @{text "trm"} and a contrived
+ version for assignments, @{text "assn"}:
- In the version of
- Nominal Isabelle described here, we also adopted the restriction from the
- Ott-tool that binding functions can only return: the empty set or empty list
- (as in case @{text PNil}), a singleton set or singleton list containing an
- atom (case @{text PVar}), or unions of atom sets or appended atom lists
- (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
- later on.
+ \begin{equation}\label{bnexp}
+ \mbox{%
+ \begin{tabular}{@ {}l@ {}}
+ \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
+ \isacommand{and} @{text "assn"} $=$\\
+ \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+ \hspace{5mm}$\mid$~@{text "ACons x::name y::name t::trm assn"}
+ \;\;\isacommand{binds} @{text "y"} \isacommand{in} @{text t}\\
+ \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
+ \isacommand{where}~@{text "bn(ANil) = []"}\\
+ \hspace{5mm}$\mid$~@{text "bn(ACons x y t as) = [atom x] @ bn(as)"}\\
+ \end{tabular}}
+ \end{equation}\smallskip
+
+ \noindent
+ In this example the term constructor @{text "ACons"} contains a binding
+ clause, and also is used in the definition of the binding function. The
+ restriction we have to impose is that the binding function can only return
+ free atoms, that is the ones that are not mentioned in a binding clause.
+ Therefore @{text "y"} cannot be used in the binding function, @{text "bn"}
+ (since it is bound in @{text "ACons"} by the binding clause), but @{text x}
+ can (since it is a free atom). This restriction is sufficient for lifting
+ the binding function to alpha-equated terms. If we would allow that @{text "bn"}
+ can return also @{text "y"}, then it would not be respectful and therefore
+ cannot be lifted.
+
+ In the version of Nominal Isabelle described here, we also adopted the
+ restriction from the Ott-tool that binding functions can only return: the
+ empty set or empty list (as in case @{text ANil}), a singleton set or
+ singleton list containing an atom (case @{text PVar} in \eqref{letpat}), or
+ unions of atom sets or appended atom lists (case @{text ACons}). This
+ restriction will simplify some automatic definitions and proofs later on.
In order to simplify our definitions of free atoms and alpha-equivalence,
we shall assume specifications
@@ -1152,7 +1197,7 @@
clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
of the lambda-terms, the completion produces
- \begin{center}
+ \[\mbox{
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
\isacommand{nominal\_datatype} @{text lam} =\\
\hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
@@ -1161,8 +1206,8 @@
\;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
\;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
\noindent
The point of completion is that we can make definitions over the binding
@@ -1174,16 +1219,16 @@
text {*
Having dealt with all syntax matters, the problem now is how we can turn
specifications into actual type definitions in Isabelle/HOL and then
- establish a reasoning infrastructure for them. As
- Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
- re-arranging the arguments of
- term-constructors so that binders and their bodies are next to each other will
- result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}.
- Therefore we will first
- extract ``raw'' datatype definitions from the specification and then define
- explicitly an alpha-equivalence relation over them. We subsequently
+ establish a reasoning infrastructure for them. As Pottier and Cheney pointed
+ out \cite{Cheney05,Pottier06}, just re-arranging the arguments of
+ term-constructors so that binders and their bodies are next to each other
+ will result in inadequate representations in cases like \mbox{@{text "Let
+ x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}}. Therefore we will
+ first extract ``raw'' datatype definitions from the specification and then
+ define explicitly an alpha-equivalence relation over them. We subsequently
construct the quotient of the datatypes according to our alpha-equivalence.
+
The ``raw'' datatype definition can be obtained by stripping off the
binding clauses and the labels from the types. We also have to invent
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
@@ -1203,18 +1248,22 @@
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
- %
+
\begin{equation}\label{ceqvt}
- @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
- \end{equation}
+ @{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
+ \end{equation}\smallskip
The first non-trivial step we have to perform is the generation of
- free-atom functions from the specification. For the
+ \emph{free-atom functions} from the specification.\footnote{Admittedly, the
+ details of our definitions are somewhat involved. However they are still
+ conceptually simple in comparison with the ``positional'' approach taken in
+ Ott \cite[Pages 88--95]{ott-jfp}, which uses \emph{occurences} and
+ \emph{partial equivalence relations} over sets of occurences.} For the
\emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
-
+
\begin{equation}\label{fvars}
\mbox{@{text "fa_ty"}$_{1..n}$}
- \end{equation}
+ \end{equation}\smallskip
\noindent
by recursion.
@@ -1222,9 +1271,9 @@
the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
we define
- \begin{center}
- @{text "fa_bn"}$_{1..m}$.
- \end{center}
+ \[
+ @{text "fa_bn"}\mbox{$_{1..m}$}.
+ \]\smallskip
\noindent
The reason for this setup is that in a deep binder not all atoms have to be
@@ -1241,110 +1290,111 @@
clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar).
Suppose the binding clause @{text bc\<^isub>i} is of the form
- \begin{center}
+ \[
\mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
- \end{center}
+ \]\smallskip
\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
- @{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\\[-2mm]
- %
+ 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 @{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
+
\begin{equation}\label{fadef}
\mbox{@{text "fa(bc\<^isub>i) \<equiv> (D - B) \<union> B'"}}.
- \end{equation}
- %
+ \end{equation}\smallskip
+
\noindent
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}
+ \]\smallskip
\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; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason
+ for the latter choice is that @{text "ty"}$_i$ is not a type that is part of the specification, and
+ we assume @{text supp} is the generic notion that characterises the free variables of
+ a type (in fact in the next section we will show that the free-variable functions we
+ define here, are equal to the support once lifted to alpha-equivalence classes).
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\\[-4mm]
- \begin{center}
+ \[\mbox{
\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}
+ @{text "bn\<^bsub>atom\<^esup> a"} & @{text "\<equiv>"} & @{text "{atom a}"}\\
+ @{text "bn\<^bsub>atom_set\<^esup> as"} & @{text "\<equiv>"} & @{text "atoms as"}\\
+ @{text "bn\<^bsub>atom_list\<^esub> as"} & @{text "\<equiv>"} & @{text "atoms (set as)"}
+ \end{tabular}}
+ \]\smallskip
- \begin{center}
- @{text "bn\<^bsub>atom\<^esub> a \<equiv> {atom a}"}\hfill
- @{text "bn\<^bsub>atom_set\<^esub> as \<equiv> atoms as"}\hfill
- @{text "bn\<^bsub>atom_list\<^esub> as \<equiv> atoms (set as)"}
- \end{center}
- %
\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}"}.
- The set @{text B} is then formally defined as\\[-4mm]
- %
- \begin{center}
+ The set @{text B} is then formally defined as
+
+ \begin{equation}\label{bdef}
@{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
- \end{center}
- %
+ \end{equation}\smallskip
+
\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}
+ where we use the auxiliary binding functions for shallow binders (that means
+ when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
+ @{text "atom list"}). The set @{text "B'"} collects all free atoms in
+ non-recursive deep binders. Let us assume these binders in the binding
+ clause @{text "bc\<^isub>i"} are
+
+ \[
\mbox{@{text "bn\<^isub>1 l\<^isub>1, \<dots>, bn\<^isub>r l\<^isub>r"}}
- \end{center}
+ \]\smallskip
\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\\[-5mm]
- %
- \begin{center}
- @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}\\[-9mm]
- \end{center}
- %
+ with @{text "l"}$_{1..r}$ $\subseteq$ @{text "b"}$_{1..p}$ (see
+ \eqref{bdef}) and none of the @{text "l"}$_{1..r}$ being among the bodies
+ @{text "d"}$_{1..q}$. The set @{text "B'"} is defined as
+
+ \begin{equation}\label{bprimedef}
+ @{text "B' \<equiv> fa_bn\<^isub>1 l\<^isub>1 \<union> ... \<union> fa_bn\<^isub>r l\<^isub>r"}
+ \end{equation}\smallskip
+
\noindent
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 in \eqref{fadef}
the set of atoms that are left unbound by the binding functions @{text
- "bn"}$_{1..m}$. We used 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
+ "bn"}$_{1..m}$, see also the definition in \eqref{bprimedef}. We used for
+ the definition of this set the functions @{text "fa_bn"}$_{1..m}$. The
+ definition for those functions needs to be extracted from the clauses the
+ user provided for @{text "bn"}$_{1..m}$ Assume the user specified a @{text
+ bn}-clause of the form
- \begin{center}
+ \[
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
- \end{center}
+ \]\smallskip
\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:
+ 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}
+ \[\mbox{
\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_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),\smallskip\\
$\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\\
+ with the recursive call @{text "bn\<^isub>i z\<^isub>i"}, and\smallskip\\
$\bullet$ & @{term "{}"} provided @{text "z\<^isub>i"} occurs in @{text "rhs"},
- but without a recursive call.
- \end{tabular}
- \end{center}
+ but without a recursive call\\
+ & (that means @{text "z\<^isub>i"} is supposed to become bound by the binding function)\\
+ \end{tabular}}
+ \]\smallskip
\noindent
For defining @{text "fa_bn (C z\<^isub>1 \<dots> z\<^isub>n)"} we just union up all these sets.
@@ -1356,77 +1406,79 @@
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}
+
+ \[\mbox{
\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]
+ @{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)"}\smallskip\\
@{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
- @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\\[1mm]
+ @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\
@{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
@{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
+
\noindent
- 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 free atoms
- of an assignment (in case of @{text "ACons"}, they are given in
- terms of @{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"}. 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 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"}.
+ 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 free atoms of an assignment
+ (in case of @{text "ACons"}, they are given in terms of @{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"}. 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 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"}.
- An interesting point in this
- 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"}-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 the alpha-equivalence relations for the raw types @{text
- "ty"}$_{1..n}$ from the specification. We write them as
+ An interesting point in this 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"}-functions to alpha-equated terms if they
+ act on atoms that are bound. In that case, these functions would \emph{not}
+ respect alpha-equivalence.
+
+ Having the free atom functions at our disposal, we can next define the
+ alpha-equivalence relations for the raw types @{text
+ "ty"}$_{1..n}$. We write them as
- \begin{center}
- @{text "\<approx>ty"}$_{1..n}$.
- \end{center}
+ \[
+ \mbox{@{text "\<approx>ty"}$_{1..n}$}.
+ \]\smallskip
\noindent
Like with the free-atom functions, we also need to
define auxiliary alpha-equivalence relations
- \begin{center}
- @{text "\<approx>bn\<^isub>"}$_{1..m}$
- \end{center}
+ \[
+ \mbox{@{text "\<approx>bn\<^isub>"}$_{1..m}$}
+ \]\smallskip
\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}
+ \[\mbox{
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{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 "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (y\<^isub>1,\<dots>, y\<^isub>n)"} & @{text "\<equiv>"} &
+ @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n y\<^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}
+ \end{tabular}}
+ \]\smallskip
The alpha-equivalence relations are defined as inductive predicates
@@ -1434,22 +1486,23 @@
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) \<dots> prems(bc\<^isub>k)"}}}
- \end{center}
+ \]\smallskip
\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}
+ The task below is to specify what the premises corresponding to a binding
+ clause are. To understand better whet the general pattern is, let us first
+ treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause
+ of the form
+
+ \[
\mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
- \end{center}
+ \]\smallskip
\noindent
- In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this
+ 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
@@ -1509,7 +1562,7 @@
lets us formally define the premise @{text P} for a non-empty binding clause as:
\begin{center}
- \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
+ \mbox{@{term "P \<equiv> alpha_set_ex (B, D) R fa (B', D')"}}\;.
\end{center}
\noindent
@@ -1582,9 +1635,9 @@
\begin{center}
\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\\
+ {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
\makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
- {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
+ {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}
\end{tabular}
\end{center}