--- a/LMCS-Paper/Paper.thy Sun Sep 11 18:04:29 2011 +0100
+++ b/LMCS-Paper/Paper.thy Mon Sep 12 21:48:26 2011 +0200
@@ -664,7 +664,7 @@
{\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)}
@{text \<pi>} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
- requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
+ requirements {\it (i)} to {\it (iv)} can be stated formally as:
\begin{defi}[Alpha-Equivalence for Set-Bindings]\label{alphaset}\mbox{}\\
\begin{tabular}{@ {\hspace{10mm}}l@ {\hspace{5mm}}rl}
@@ -899,6 +899,19 @@
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
the first equation of Theorem~\ref{suppabs}.
+ Recall the definition of support \eqref{suppdef}, and note the difference between
+ the support of a ``raw'' pair and an abstraction
+
+ \[
+ @{term "supp (as, x) = supp as \<union> supp x"}\hspace{15mm}
+ @{term "supp (Abs_set as x) = supp x - as"}
+ \]\smallskip
+
+ \noindent
+ While the permutation operations behave in both cases the same (the permutation
+ is just moved to the arguments), the notion of equality is different for pairs and
+ abstractions. Therefore we have different supports.
+
The method of first considering abstractions of the form @{term "Abs_set as
x"} etc is motivated by the fact that we can conveniently establish at the
Isabelle/HOL level properties about them. It would be extremely laborious
@@ -1022,25 +1035,27 @@
Shallow binders are just labels. The restriction we need to impose on them
is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the
labels must either refer to atom types or to sets of atom types; in case of
- \isacommand{binds} the labels must refer to atom types or lists of atom
+ \isacommand{binds} the labels must refer to atom types or to lists of atom
types. Two examples for the use of shallow binders are the specification of
lambda-terms, where a single name is bound, and type-schemes, where a finite
set of names is bound:
\[\mbox{
- \begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}}
+ \begin{tabular}{@ {}c@ {\hspace{8mm}}c@ {}}
\begin{tabular}{@ {}l}
\isacommand{nominal\_datatype} @{text lam} $=$\\
\hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\
\hspace{2mm}$\mid$~@{text "App lam lam"}\\
\hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}%
\isacommand{binds} @{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{3mm}%
+ \hspace{2mm}\phantom{$\mid$}~@{text "TVar name"}\\
+ \hspace{2mm}$\mid$~@{text "TFun ty ty"}\\
+ \isacommand{and}~@{text "tsc ="}\\
+ \hspace{2mm}\phantom{$\mid$}~@{text "TAll xs::(name fset) T::ty"}\hspace{3mm}%
\isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\
\end{tabular}
\end{tabular}}
@@ -1176,16 +1191,16 @@
\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 permit that @{text "bn"}
- can also return @{text "y"}, then it would not be respectful and therefore
- cannot be lifted.
+ In this example the term constructor @{text "ACons'"} has four arguments and
+ contains a binding clause. This constructor is also 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 permit that @{text "bn"} can also return @{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
@@ -1499,7 +1514,7 @@
\noindent
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
+ clause are. To understand better what the general pattern is, let us first
treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause
of the form
@@ -1508,27 +1523,33 @@
\]\smallskip
\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
-
+ 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 the arguments @{text
+ "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text
+ "z\<PRIME>"}$_{1..n}$ of the term-constructor. 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}
+ \end{equation}\smallskip
\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
+ 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 "="}. Again the
+ latter is because @{text "ty\<^isub>i"} is not part of the specified types
+ and alpha-equivalence of any previously defined type is supposed to coincide
+ with equality. This lets us now 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}
+ \]\smallskip
\noindent
We will use the unfolded version in the examples below.
@@ -1537,7 +1558,7 @@
\begin{equation}\label{nonempty}
\mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
- \end{equation}
+ \end{equation}\smallskip
\noindent
In this case we define a premise @{text P} using the relation
@@ -1550,83 +1571,82 @@
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}
+ \]\smallskip
\noindent
with the 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}
+ \]\smallskip
\noindent
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{center}
+ \[
\mbox{@{term "P \<equiv> alpha_set_ex (B, D) R fa (B', D')"}}\;.
- \end{center}
+ \]\smallskip
\noindent
This premise accounts for alpha-equivalence of the bodies of the binding
- clause.
- However, in case the binders have non-recursive deep binders, this premise
- is not enough:
- 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
- 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
+ clause. However, in case the binders have non-recursive deep binders, this
+ premise is not enough: 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 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}
+ \]\smallskip
\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
+ The tuple @{text L} consists then of all these binders @{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
- \begin{center}
+ \[
@{text "prems(bc\<^isub>i) \<equiv> P \<and> L R' L'"}
- \end{center}
+ \]\smallskip
\noindent
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}
+ \[
@{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}$,
then the corresponding 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}
+ \]\smallskip
\noindent
In this clause the relations @{text "R"}$_{1..s}$ are given by
- \begin{center}
+ \[\mbox{
\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},\\
+ is a recursive argument of @{text C},\smallskip\\
$\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},\\
+ and is a non-recursive argument of @{text C},\smallskip\\
$\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\\
+ with the recursive call @{text "bn\<^isub>i x\<^isub>i"} and\smallskip\\
$\bullet$ & @{text True} provided @{text "z\<^isub>i"} occurs in @{text rhs} but without a
recursive call.
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
\noindent
This completes the definition of alpha-equivalence. As a sanity check, we can show
@@ -1638,30 +1658,30 @@
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$ with the following clauses:
- \begin{center}
+ \[\mbox{
\begin{tabular}{@ {}c @ {}}
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
- {@{term "alpha_lst_ex (bn as, t) alpha_trm fa_trm (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')"} &
+ \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\\
+ \\
\makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
- {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}
- \end{tabular}
- \end{center}
+ {@{term "alpha_lst_ex (bn as, ast) alpha_trm2 fa_trm2 (bn as', ast')"}}}\\
+ \\
- \begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
- {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
- \end{tabular}
- \end{center}
+ {@{text "a = a'"} & \hspace{5mm}@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
+ \end{tabular}\\
+ \\
- \begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
- {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
+ {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & \hspace{5mm}@{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
\end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
\noindent
Note the difference between $\approx_{\textit{assn}}$ and
@@ -1677,37 +1697,81 @@
section {* Establishing the Reasoning Infrastructure *}
text {*
- Having made all necessary definitions for raw terms, we can start
- with establishing the reasoning infrastructure for the alpha-equated types
- @{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch
- in this section the proofs we need for establishing this infrastructure. One
- main point of our work is that we have completely automated these proofs in Isabelle/HOL.
+ Having made all necessary definitions for raw terms, we can start with
+ establishing the reasoning infrastructure for the alpha-equated types @{text
+ "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We
+ give in this section and the next the proofs we need for establishing this
+ infrastructure. One main point of our work is that we have completely
+ automated these proofs in Isabelle/HOL.
+
+ First we establish that the free-variable functions, the binding functions and the
+ alpha-equivalences are equivariant.
- First we establish that the
- alpha-equivalence relations defined in the previous section are
- equivalence relations.
+ \begin{lem}\mbox{}\\
+ @{text "(i)"} The functions @{text "fa_ty"}$_{1..n}$, @{text "fa_bn"}$_{1..m}$ and
+ @{text "bn"}$_{1..m}$ are equivariant.\\
+ @{text "(ii)"} The relations @{text "\<approx>ty"}$_{1..n}$ and
+ @{text "\<approx>bn"}$_{1..m}$ are equivariant.
+ \end{lem}
+
+ \begin{proof}
+ The function package of Isabelle/HOL allows us to prove the first part is by mutual
+ induction over the definitions of the functions. The second is by a straightforward
+ induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using
+ the first part.
+ \end{proof}
+
+ \noindent
+ Next we establish that the alpha-equivalence relations defined in the
+ previous section are equivalence relations.
\begin{lem}\label{equiv}
- Given the raw types @{text "ty"}$_{1..n}$ and binding functions
- @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and
- @{text "\<approx>bn"}$_{1..m}$ are equivalence relations. and equivariant.
+ The relations @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ are
+ equivalence relations.
\end{lem}
\begin{proof}
The proof is by mutual induction over the definitions. The non-trivial
cases involve premises built up by $\approx_{\textit{set}}$,
$\approx_{\textit{set+}}$ and $\approx_{\textit{list}}$. They
- can be dealt with as in Lemma~\ref{alphaeq}.
+ can be dealt with as in Lemma~\ref{alphaeq}. However, the transitivity
+ case needs in addition the fact that the relations are equivariant.
\end{proof}
\noindent
We can feed this lemma into our quotient package and obtain new types @{text
"ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$.
+
We also obtain definitions for the term-constructors @{text
- "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
- "C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
- "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the binding functions @{text
- "bn"}$^\alpha_{1..m}$. However, these definitions are not really useful to the
+ "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text "C"}$_{1..k}$,
+ and similar definitions for the free-atom functions @{text
+ "fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
+ binding functions @{text "bn"}$^\alpha_{1..m}$. For this we have to show
+ by induction over the definitions of alpha-equivalences that the ``raw''
+ functions are respectful. This means we need to establish that
+
+ \[\mbox{
+ \begin{tabular}{lll}
+ @{text "x \<approx>ty\<^isub>i x'"} & implies & @{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x'"}\\
+ @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x'"}\\
+ @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "bn\<^isub>j x = bn\<^isub>j x'"}\\
+ \end{tabular}
+ }\]\smallskip
+
+ \noindent
+ holds whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"} is defined. A
+ similar property is needed for the constructors @{text "C"}$_{1..k}$. In order
+ to establish it we need to prove that
+
+ \[\mbox{
+ \begin{tabular}{lll}
+ @{text "x \<approx>ty\<^isub>l x'"} & implies & @{text "x \<approx>bn\<^isub>j x'"}\\
+ \end{tabular}
+ }\]\smallskip
+
+ \noindent
+ The respectfulness properties are crucial, ... ???
+ However, these definitions are not really useful to the
user, since they are given in terms of the isomorphisms we obtained by
creating new types in Isabelle/HOL (recall the picture shown in the
Introduction).
@@ -1716,19 +1780,19 @@
term-constructors are not
equal, that is
- \begin{equation}\label{distinctalpha}
+ \[\label{distinctalpha}
\mbox{@{text "C"}$^\alpha$~@{text "x\<^isub>1 \<dots> x\<^isub>r"}~@{text "\<noteq>"}~%
@{text "D"}$^\alpha$~@{text "y\<^isub>1 \<dots> y\<^isub>s"}}
- \end{equation}
+ \]\smallskip
\noindent
whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
In order to derive this fact, we use the definition of alpha-equivalence
and establish that
- \begin{equation}\label{distinctraw}
+ \[\label{distinctraw}
\mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r"}\;$\not\approx$@{text ty}\;@{text "D y\<^isub>1 \<dots> y\<^isub>s"}}
- \end{equation}
+ \]\smallskip
\noindent
holds for the corresponding raw term-constructors.
@@ -1774,20 +1838,20 @@
Having established respectfulness for the raw term-constructors, the
quotient package is able to automatically deduce \eqref{distinctalpha} from
- \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
+ \eqref{distinctraw}. ??? Having the facts \eqref{fnresp} at our disposal, we can
also lift properties that characterise when two raw terms of the form
- %
- \begin{center}
- @{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}
- \end{center}
+
+ \[
+ \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
+ \]\smallskip
\noindent
are alpha-equivalent. This gives us conditions when the corresponding
alpha-equated terms are \emph{equal}, namely
- \begin{center}
+ \[
@{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
- \end{center}
+ \]\smallskip
\noindent
We call these conditions as \emph{quasi-injectivity}. They correspond to
@@ -1803,8 +1867,8 @@
As a result we can add the equations
\begin{equation}\label{calphaeqvt}
- @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
- \end{equation}
+ @{text "\<pi> \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (\<pi> \<bullet> x\<^isub>1) \<dots> (\<pi> \<bullet> x\<^isub>r)"}
+ \end{equation}\smallskip
\noindent
to our infrastructure. In a similar fashion we can lift the defining equations
@@ -1821,7 +1885,7 @@
\begin{equation}\label{weakinduct}
\mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
- \end{equation}
+ \end{equation} \smallskip
\noindent
whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$
@@ -1830,7 +1894,7 @@
\begin{equation}\label{weakprem}
\mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}}
- \end{equation}
+ \end{equation}\smallskip
\noindent
in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
@@ -1840,24 +1904,25 @@
can first show that the free-atom functions and binding functions are
equivariant, namely
- \begin{center}
- \begin{tabular}{rcl@ {\hspace{10mm}}rcl}
- @{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} &
- @{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\
- @{text "p \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\
- \end{tabular}
- \end{center}
+ \[\mbox{
+ \begin{tabular}{rcl}
+ @{text "\<pi> \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (\<pi> \<bullet> x)"}\\
+ @{text "\<pi> \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
+ @{text "\<pi> \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (\<pi> \<bullet> x)"}\\
+ \end{tabular}}
+ \]
+
\noindent
- These properties can be established using the induction principle for the types @{text "ty\<AL>"}$_{1..n}$.
- in \eqref{weakinduct}.
- Having these equivariant properties established, we can
- show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in
- the support of its arguments, that means
+ These properties can be established using the induction principle for the
+ types @{text "ty\<AL>"}$_{1..n}$. in \eqref{weakinduct}. Having these
+ equivariant properties established, we can show that the support of
+ term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
+ arguments, that means
- \begin{center}
+ \[
@{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"}
- \end{center}
+ \]\smallskip
\noindent
holds. This allows us to prove by induction that
@@ -2244,37 +2309,42 @@
text {*
To our knowledge the earliest usage of general binders in a theorem prover
- is described in \cite{NaraschewskiNipkow99} about a formalisation of the
- algorithm W. This formalisation implements binding in type-schemes using a
- de-Bruijn indices representation. Since type-schemes in W contain only a single
- place where variables are bound, different indices do not refer to different binders (as in the usual
- de-Bruijn representation), but to different bound variables. A similar idea
- has been recently explored for general binders in the locally nameless
- approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist
- of two numbers, one referring to the place where a variable is bound, and the
- other to which variable is bound. The reasoning infrastructure for both
- representations of bindings comes for free in theorem provers like Isabelle/HOL or
- Coq, since the corresponding term-calculi can be implemented as ``normal''
- datatypes. However, in both approaches it seems difficult to achieve our
- fine-grained control over the ``semantics'' of bindings (i.e.~whether the
- order of binders should matter, or vacuous binders should be taken into
- account). To do so, one would require additional predicates that filter out
- unwanted terms. Our guess is that such predicates result in rather
- intricate formal reasoning.
+ is described by Nara\-schew\-ski and Nipkow \cite{NaraschewskiNipkow99} with a
+ formalisation of the algorithm W. This formalisation implements binding in
+ type-schemes using a de-Bruijn indices representation. Since type-schemes in
+ W contain only a single place where variables are bound, different indices
+ do not refer to different binders (as in the usual de-Bruijn
+ representation), but to different bound variables. A similar idea has been
+ recently explored for general binders by Chargu\'eraud in the locally nameless
+ approach to
+ binding \cite{chargueraud09}. There, de-Bruijn indices consist of two
+ numbers, one referring to the place where a variable is bound, and the other
+ to which variable is bound. The reasoning infrastructure for both
+ representations of bindings comes for free in theorem provers like
+ Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented
+ as ``normal'' datatypes. However, in both approaches it seems difficult to
+ achieve our fine-grained control over the ``semantics'' of bindings
+ (i.e.~whether the order of binders should matter, or vacuous binders should
+ be taken into account). To do so, one would require additional predicates
+ that filter out unwanted terms. Our guess is that such predicates result in
+ rather intricate formal reasoning. We are not aware of any non-trivial
+ formalisation that uses Chargu\'eraud's idea.
+
Another technique for representing binding is higher-order abstract syntax
- (HOAS). , which for example is implemented in the Twelf system.
- This representation
- technique supports very elegantly many aspects of \emph{single} binding, and
- impressive work has been done that uses HOAS for mechanising the metatheory
- of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
- binders of SML are represented in this work. Judging from the submitted
- Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
- binding constructs where the number of bound variables is not fixed. For example
- In the second part of this challenge, @{text "Let"}s involve
- patterns that bind multiple variables at once. In such situations, HOAS
- seems to have to resort to the iterated-single-binders-approach with
- all the unwanted consequences when reasoning about the resulting terms.
+ (HOAS), which for example is implemented in the Twelf system. This
+ representation technique supports very elegantly many aspects of
+ \emph{single} binding, and impressive work by Lee et al has been done that
+ uses HOAS for mechanising the metatheory of SML~\cite{LeeCraryHarper07}. We
+ are, however, not aware how multiple binders of SML are represented in this
+ work. Judging from the submitted Twelf-solution for the POPLmark challenge,
+ HOAS cannot easily deal with binding constructs where the number of bound
+ variables is not fixed. For example In the second part of this challenge,
+ @{text "Let"}s involve patterns that bind multiple variables at once. In
+ such situations, HOAS seems to have to resort to the
+ iterated-single-binders-approach with all the unwanted consequences when
+ reasoning about the resulting terms.
+
Two formalisations involving general binders have been
performed in older
@@ -2285,117 +2355,126 @@
the need to ``unbind'' variables. This can be done in one step with our
general binders described in this paper, but needs a cumbersome
iteration with single binders. The resulting formal reasoning turned out to
- be rather unpleasant. The hope is that the extension presented in this paper
- is a substantial improvement.
+ be rather unpleasant.
- The most closely related work to the one presented here is the Ott-tool
- \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
- front-end for creating \LaTeX{} documents from specifications of
- term-calculi involving general binders. For a subset of the specifications
- Ott can also generate theorem prover code using a raw representation of
- terms, and in Coq also a locally nameless representation. The developers of
- this tool have also put forward (on paper) a definition for
- alpha-equivalence of terms that can be specified in Ott. This definition is
- rather different from ours, not using any nominal techniques. To our
- knowledge there is no concrete mathematical result concerning this
- notion of alpha-equivalence. Also the definition for the
- notion of free variables
- is work in progress.
+ The most closely related work to the one presented here is the Ott-tool by
+ Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
+ \cite{Pottier06}. Ott is a nifty front-end for creating \LaTeX{} documents
+ from specifications of term-calculi involving general binders. For a subset
+ of the specifications Ott can also generate theorem prover code using a raw
+ representation of terms, and in Coq also a locally nameless
+ representation. The developers of this tool have also put forward (on paper)
+ a definition for alpha-equivalence and free variables for terms that can be
+ specified in Ott. This definition is rather different from ours, not using
+ any nominal techniques. To our knowledge there is no concrete mathematical
+ result concerning this notion of alpha-equivalence and free variables. We
+ have proved that our definitions lead to alpha-equated terms, whose support
+ is as expected (that means bound names are removed from the support). We
+ also showed that our specifications lift from a raw type to a type of
+ alpha-equivalence classes. For this we were able to establish then every
+ term-constructor and function is repectful w.r.t.~alpha-equivalence.
- Although we were heavily inspired by the syntax of Ott,
- its definition of alpha-equi\-valence is unsuitable for our extension of
- Nominal Isabelle. First, it is far too complicated to be a basis for
- automated proofs implemented on the ML-level of Isabelle/HOL. Second, it
- covers cases of binders depending on other binders, which just do not make
- sense for our alpha-equated terms. Third, it allows empty types that have no
- meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
- binding clauses. In Ott you specify binding clauses with a single body; we
- allow more than one. We have to do this, because this makes a difference
- for our notion of alpha-equivalence in case of \isacommand{binds (set)} and
- \isacommand{binds (set+)}.
+ Although we were heavily inspired by the syntax of Ott, its definition of
+ alpha-equi\-valence is unsuitable for our extension of Nominal
+ Isabelle. First, it is far too complicated to be a basis for automated
+ proofs implemented on the ML-level of Isabelle/HOL. Second, it covers cases
+ of binders depending on other binders, which just do not make sense for our
+ alpha-equated terms. Third, it allows empty types that have no meaning in a
+ HOL-based theorem prover. We also had to generalise slightly Ott's binding
+ clauses. In Ott one specifies binding clauses with a single body; we allow
+ more than one. We have to do this, because this makes a difference for our
+ notion of alpha-equivalence in case of \isacommand{binds (set)} and
+ \isacommand{binds (set+)}. Consider the examples
- Consider the examples
-
- \begin{center}
+ \[\mbox{
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
\isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
\isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"},
\isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
- \end{tabular}
- \end{center}
-
- \noindent
- In the first term-constructor we have a single
- body that happens to be ``spread'' over two arguments; in the second term-constructor we have
- two independent bodies in which the same variables are bound. As a result we
- have
-
- \begin{center}
- \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
- @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
- @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
- @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
- @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \]\smallskip
\noindent
- and therefore need the extra generality to be able to distinguish between
- both specifications.
- Because of how we set up our definitions, we also had to impose some restrictions
- (like a single binding function for a deep binder) that are not present in Ott.
- Our
- expectation is that we can still cover many interesting term-calculi from
- programming language research, for example Core-Haskell.
+ In the first term-constructor we have a single body that happens to be
+ ``spread'' over two arguments; in the second term-constructor we have two
+ independent bodies in which the same variables are bound. As a result we
+ have\footnote{Assuming @{term "a \<noteq> b"}, there is no permutation that can
+ make @{text "(a, b)"} equal with @{text "(a, b)"} and @{text "(b, a)"}, but
+ there are two permutations so that we can make @{text "(a, b)"} and @{text
+ "(a, b)"} equal with one permutation, and @{text "(a, b)"} and @{text "(b,
+ a)"} with the other.}
+
+
+ \[\mbox{
+ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+ @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
+ @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}
+ \end{tabular}}
+ \]\smallskip
+
+ \noindent
+ but
- Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for
- representing terms with general binders inside OCaml. This language is
- implemented as a front-end that can be translated to OCaml with the help of
- a library. He presents a type-system in which the scope of general binders
- can be specified using special markers, written @{text "inner"} and
- @{text "outer"}. It seems our and his specifications can be
- inter-translated as long as ours use the binding mode
- \isacommand{binds} only.
- However, we have not proved this. Pottier gives a definition for
+ \[\mbox{
+ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+ @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
+ @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+ \end{tabular}}
+ \]\smallskip
+
+ \noindent
+ and therefore need the extra generality to be able to distinguish between
+ both specifications. Because of how we set up our definitions, we also had
+ to impose some restrictions (like a single binding function for a deep
+ binder) that are not present in Ott. Our expectation is that we can still
+ cover many interesting term-calculi from programming language research, for
+ example Core-Haskell. ???
+
+ Pottier presents a programming language, called C$\alpha$ml, for
+ representing terms with general binders inside OCaml \cite{Pottier06}. This
+ language is implemented as a front-end that can be translated to OCaml with
+ the help of a library. He presents a type-system in which the scope of
+ general binders can be specified using special markers, written @{text
+ "inner"} and @{text "outer"}. It seems our and his specifications can be
+ inter-translated as long as ours use the binding mode \isacommand{binds}
+ only. However, we have not proved this. Pottier gives a definition for
alpha-equivalence, which also uses a permutation operation (like ours).
Still, this definition is rather different from ours and he only proves that
- it defines an equivalence relation. A complete
- reasoning infrastructure is well beyond the purposes of his language.
- Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}.
-
- In a slightly different domain (programming with dependent types), the
- paper \cite{Altenkirch10} presents a calculus with a notion of
- alpha-equivalence related to our binding mode \isacommand{binds (set+)}.
- The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
- has a more operational flavour and calculates a partial (renaming) map.
- In this way, the definition can deal with vacuous binders. However, to our
- best knowledge, no concrete mathematical result concerning this
- definition of alpha-equivalence has been proved.
+ it defines an equivalence relation. A complete reasoning infrastructure is
+ well beyond the purposes of his language. Similar work for Haskell with
+ similar results was reported by Cheney \cite{Cheney05a} and more recently
+ by ???
+
+ In a slightly different domain (programming with dependent types),
+ Altenkirch et al present a calculus with a notion of alpha-equivalence
+ related to our binding mode \isacommand{binds (set+)} \cite{Altenkirch10}.
+ Their definition is similar to the one by Pottier, except that it has a more
+ operational flavour and calculates a partial (renaming) map. In this way,
+ the definition can deal with vacuous binders. However, to our best
+ knowledge, no concrete mathematical result concerning this definition of
+ alpha-equivalence has been proved.
*}
section {* Conclusion *}
text {*
- Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).
+ %%Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).
- We have presented an extension of Nominal Isabelle for dealing with
- general binders, that is term-constructors having multiple bound
- variables. For this extension we introduced new definitions of
- alpha-equivalence and automated all necessary proofs in Isabelle/HOL.
- To specify general binders we used the specifications from Ott, but extended them
- in some places and restricted
- them in others so that they make sense in the context of alpha-equated terms.
- We also introduced two binding modes (set and set+) that do not
- exist in Ott.
- We have tried out the extension with calculi such as Core-Haskell, type-schemes
- and approximately a dozen of other typical examples from programming
- language research~\cite{SewellBestiary}.
- The code
- will eventually become part of the next Isabelle distribution.\footnote{For the moment
- it can be downloaded from the Mercurial repository linked at
+ We have presented an extension of Nominal Isabelle for dealing with general
+ binders, that is term-constructors having multiple bound variables. For this
+ extension we introduced new definitions of alpha-equivalence and automated
+ all necessary proofs in Isabelle/HOL. To specify general binders we used
+ the syntax from Ott, but extended it in some places and restricted
+ it in others so that they make sense in the context of alpha-equated
+ terms. We also introduced two binding modes (set and set+) that do not exist
+ in Ott. We have tried out the extension with calculi such as Core-Haskell,
+ type-schemes and approximately a dozen of other typical examples from
+ programming language research~\cite{SewellBestiary}. The code will
+ eventually become part of the next Isabelle distribution.\footnote{It
+ can be downloaded already from the Mercurial repository linked at
\href{http://isabelle.in.tum.de/nominal/download}
{http://isabelle.in.tum.de/nominal/download}.}
@@ -2412,7 +2491,9 @@
datatype definitions allow one to specify, for instance, the function kinds
in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
- achieve this, we need a slightly more clever implementation than we have at the moment.
+ achieve this, we need more clever implementation than we have
+ at the moment. However, really lifting this restriction will involve major
+ work on the datatype package of Isabelle/HOL.
A more interesting line of investigation is whether we can go beyond the
simple-minded form of binding functions that we adopted from Ott. At the moment, binding
@@ -2420,18 +2501,18 @@
of atom sets (similarly for lists). It remains to be seen whether
properties like
- \begin{center}
- @{text "fa_ty x = bn x \<union> fa_bn x"}.
- \end{center}
+ \[
+ \mbox{@{text "fa_ty x = bn x \<union> fa_bn x"}}
+ \]\smallskip
\noindent
allow us to support more interesting binding functions.
We have also not yet played with other binding modes. For example we can
- imagine that there is need for a binding mode where instead of lists, we
- abstract lists of distinct elements. Once we feel confident about such
- binding modes, our implementation can be easily extended to accommodate
- them.\medskip
+ imagine that there is need for a binding mode where instead of usual lists,
+ we abstract lists of distinct elements (the corresponding type @{text
+ "dlist"} already exists in the library of Isabelle/HOL). We expect the
+ presented work can be easily extended to accommodate them.\medskip
\noindent
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for many