--- a/Paper/Paper.thy Wed Oct 06 08:13:09 2010 +0100
+++ b/Paper/Paper.thy Wed Oct 06 21:32:44 2010 +0100
@@ -124,9 +124,10 @@
where @{text z} does not occur freely in the type. In this paper we will
give a general binding mechanism and associated notion of $\alpha$-equivalence
that can be used to faithfully represent this kind of binding in Nominal
- Isabelle. The difficulty of finding the right notion for $\alpha$-equivalence
- can be appreciated in this case by considering that the definition given by
- Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+ Isabelle.
+ %The difficulty of finding the right notion for $\alpha$-equivalence
+ %can be appreciated in this case by considering that the definition given by
+ %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
However, the notion of $\alpha$-equivalence that is preserved by vacuous
binders is not always wanted. For example in terms like
@@ -240,7 +241,7 @@
where no clause for variables is given. Arguably, such specifications make
some sense in the context of Coq's type theory (which Ott supports), but not
at all in a HOL-based environment where every datatype must have a non-empty
- set-theoretic model \cite{Berghofer99}.
+ set-theoretic model. % \cite{Berghofer99}.
Another reason is that we establish the reasoning infrastructure
for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning
@@ -261,14 +262,14 @@
to a variable bound somewhere else, are not excluded by Ott, but we have
to).
- Our insistence on reasoning with $\alpha$-equated terms comes from the
- wealth of experience we gained with the older version of Nominal Isabelle:
- for non-trivial properties, reasoning with $\alpha$-equated terms is much
- easier than reasoning with raw terms. The fundamental reason for this is
- that the HOL-logic underlying Nominal Isabelle allows us to replace
- ``equals-by-equals''. In contrast, replacing
- ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
- requires a lot of extra reasoning work.
+ %Our insistence on reasoning with $\alpha$-equated terms comes from the
+ %wealth of experience we gained with the older version of Nominal Isabelle:
+ %for non-trivial properties, reasoning with $\alpha$-equated terms is much
+ %easier than reasoning with raw terms. The fundamental reason for this is
+ %that the HOL-logic underlying Nominal Isabelle allows us to replace
+ %``equals-by-equals''. In contrast, replacing
+ %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
+ %requires a lot of extra reasoning work.
Although in informal settings a reasoning infrastructure for $\alpha$-equated
terms is nearly always taken for granted, establishing it automatically in
@@ -349,9 +350,10 @@
and lambda are lifted to the quotient level.) This construction, of course,
only works if $\alpha$-equivalence is indeed an equivalence relation, and the
``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
- For example, we will not be able to lift a bound-variable function. Although
- this function can be defined for raw terms, it does not respect
- $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting
+ %For example, we will not be able to lift a bound-variable function. Although
+ %this function can be defined for raw terms, it does not respect
+ %$\alpha$-equivalence and therefore cannot be lifted.
+ To sum up, every lifting
of theorems to the quotient level needs proofs of some respectfulness
properties (see \cite{Homeier05}). In the paper we show that we are able to
automate these proofs and as a result can automatically establish a reasoning
@@ -379,7 +381,7 @@
The main improvement over Ott is that we introduce three binding modes
(only one is present in Ott), provide definitions for $\alpha$-equivalence and
for free variables of our terms, and also derive a reasoning infrastructure
- about our specifications inside Isabelle/HOL.
+ for our specifications inside Isabelle/HOL.
%\begin{figure}
@@ -448,7 +450,7 @@
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
- where the generic type @{text "\<beta>"} stands for the type of the object
+ where the generic type @{text "\<beta>"} is the type of the object
over which the permutation
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}},
@@ -504,9 +506,9 @@
swapping two fresh atoms, say @{text a} and @{text b}, leaves
@{text x} unchanged:
- \begin{property}\label{swapfreshfresh}
+ \begin{myproperty}\label{swapfreshfresh}
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
- \end{property}
+ \end{myproperty}
%While often the support of an object can be relatively easily
%described, for example for atoms, products, lists, function applications,
@@ -546,11 +548,11 @@
%The main point of @{text supports} is that we can establish the following
%two properties.
%
- %\begin{property}\label{supportsprop}
+ %\begin{myproperty}\label{supportsprop}
%Given a set @{text "as"} of atoms.
%{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
%{\it (ii)} @{thm supp_supports[no_vars]}.
- %\end{property}
+ %\end{myproperty}
%
%Another important notion in the nominal logic work is \emph{equivariance}.
%For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
@@ -589,16 +591,16 @@
proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
- \begin{property}\label{supppermeq}
+ \begin{myproperty}\label{supppermeq}
@{thm[mode=IfThen] supp_perm_eq[no_vars]}
- \end{property}
+ \end{myproperty}
- \begin{property}\label{avoiding}
+ \begin{myproperty}\label{avoiding}
For a finite set @{text as} and a finitely supported @{text x} with
@{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
@{term "supp x \<sharp>* p"}.
- \end{property}
+ \end{myproperty}
\noindent
The idea behind the second property is that given a finite set @{text as}
@@ -760,15 +762,15 @@
representing $\alpha$-equivalence classes of pairs of type
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
(in the third case).
- The elements in these types will be, respectively, written as:
-
- \begin{center}
- @{term "Abs_set as x"} \hspace{5mm}
- @{term "Abs_res as x"} \hspace{5mm}
- @{term "Abs_lst as x"}
- \end{center}
-
- \noindent
+ The elements in these types will be, respectively, written as
+ %
+ %\begin{center}
+ @{term "Abs_set as x"}, %\hspace{5mm}
+ @{term "Abs_res as x"} and %\hspace{5mm}
+ @{term "Abs_lst as x"},
+ %\end{center}
+ %
+ %\noindent
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will
call the types \emph{abstraction types} and their elements
\emph{abstractions}. The important property we need to derive is the support of
@@ -875,7 +877,8 @@
text {*
Our choice of syntax for specifications is influenced by the existing
- datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
+ datatype package of Isabelle/HOL %\cite{Berghofer99}
+ and by the syntax of the
Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
collection of (possibly mutual recursive) type declarations, say @{text
"ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
@@ -975,7 +978,9 @@
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). For binders we distinguish between
+ 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 is that in case of
\isacommand{bind (set)} and \isacommand{bind (res)} the labels must either
@@ -1108,7 +1113,7 @@
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 infrastructure for
- $\alpha$-equated terms, it can permit such specifications.)
+ $\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
@@ -1181,10 +1186,11 @@
where @{term ty} is the type used in the quotient construction for
@{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}.
- 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 in-depth description of the datatype package
- in Isabelle/HOL). We subsequently define each of the user-specified binding
+ %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 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
@@ -1674,15 +1680,16 @@
and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
@{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
implication by applying the corresponding rule in our $\alpha$-equivalence
- definition and by establishing the following auxiliary facts
+ definition and by establishing the following auxiliary implications %facts
%
\begin{equation}\label{fnresp}
\mbox{%
- \begin{tabular}{l}
- @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\
- @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\
- @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
- @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
+ \begin{tabular}{ll@ {\hspace{7mm}}ll}
+ \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} &
+ \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\
+
+ \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} &
+ \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\
\end{tabular}}
\end{equation}
@@ -1710,11 +1717,11 @@
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}
-
- \noindent
+ %\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}
+ %
+ %\noindent
We call these conditions as \emph{quasi-injectivity}. They correspond to
the premises in our $\alpha$-equivalence relations.
@@ -1744,11 +1751,11 @@
for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
of the form
%
- \begin{equation}\label{weakinduct}
+ %\begin{equation}\label{weakinduct}
\mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
- \end{equation}
-
- \noindent
+ %\end{equation}
+ %
+ %\noindent
whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$
have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each
term constructor @{text "C"}$^\alpha$ a premise of the form
@@ -1766,36 +1773,38 @@
equivariant, namely
%
\begin{center}
- \begin{tabular}{rcl}
- @{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\
+ \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)"}\\
- @{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}
\end{tabular}
\end{center}
-
+ %
\noindent
- These properties can be established using the induction principle
- in \eqref{weakinduct}.
+ These properties can be established using the induction principle.
+ %%in \eqref{weakinduct}.
Having these equivariant properties established, we can
- show for every term-constructor @{text "C\<^sup>\<alpha>"} that
+ 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 x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}
+ @{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}
\noindent
- holds. This together with Property~\ref{supportsprop} allows us to prove
- that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported,
- namely @{text "finite (supp x)"}. This can be again shown by induction
- over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of
+ holds. This allows us to prove by induction that
+ every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported.
+ %This can be again shown by induction
+ %over @{text "ty\<AL>"}$_{1..n}$.
+ Lastly, we can show that the support of
elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
This fact is important in a nominal setting, but also provides evidence
that our notions of free-atoms and $\alpha$-equivalence are correct.
- \begin{lemma}
- For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have
- @{text "supp x = fa_ty\<AL>\<^isub>i x"}.
- \end{lemma}
+ \begin{theorem}
+ For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
+ @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
+ \end{theorem}
\begin{proof}
The proof is by induction. In each case
@@ -1888,170 +1897,270 @@
section {* Strong Induction Principles *}
text {*
- In the previous section we were able to provide induction principles that
- allow us to perform structural inductions over $\alpha$-equated terms.
- We call such induction principles \emph{weak}, because in case of the
- term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"},
+ In the previous section we derived induction principles for $\alpha$-equated terms.
+ We call such induction principles \emph{weak}, because for a
+ term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
the induction hypothesis requires us to establish the implications \eqref{weakprem}.
The problem with these implications is that in general they are difficult to establish.
- The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}
- (for example we cannot assume the variable convention for them).
+ The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}.
+ %%(for example we cannot assume the variable convention for them).
In \cite{UrbanTasson05} we introduced a method for automatically
strengthening weak induction principles for terms containing single
binders. These stronger induction principles allow the user to make additional
assumptions about binders.
- These additional assumptions amount to a formal
- version of the informal variable convention for binders. A natural question is
- whether we can also strengthen the weak induction principles involving
- the general binders presented here. We will indeed be able to so, but for this we need an
- additional notion for permuting deep binders.
-
- Given a binding function @{text "bn"} we define an auxiliary permutation
- operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
- Assuming a clause of @{text bn} is given as
+ %These additional assumptions amount to a formal
+ %version of the informal variable convention for binders.
+ To sketch how this strengthening extends to the case of multiple binders, we use as
+ running example the term-constructors @{text "Lam"} and @{text "Let"}
+ from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"},
+ the stronger induction principles establish properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"}
+ where the additional parameter @{text c} controls
+ which freshness assumptions the binders should satisfy. For the two term constructors
+ this means that the user has to establish in inductions the implications
%
\begin{center}
- @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"},
+ \begin{tabular}{l}
+ @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\
+ @{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"}
+ \end{tabular}
\end{center}
- \noindent
- then we define
+ In \cite{UrbanTasson05} we showed how the weaker induction principles imply
+ the stronger ones. This was done by some quite complicated, nevertheless automated,
+ induction proofs. In this paper we simplify this work by leveraging the automated proof
+ methods from the function package of Isabelle/HOL generates.
+
+ The reasoning principle we employ here is well-founded induction. For this we have to discharge
+ two proof obligations: one is that we have
+ well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in
+ every induction step and the other is that we have covered all cases.
+ As measures we use are the size functions
+ @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are
+ all well-founded. It is straightforward to establish that these measures decrease
+ in every induction step.
+
+ What is left to show is that we covered all cases. To do so, we use
+ a cases lemma derived for each type, which for the terms in \eqref{letpat}
+ is of the form
+ %
+ \begin{equation}\label{weakcases}
+ \infer{@{text "P\<^bsub>trm\<^esub>"}}
+ {\begin{array}{l@ {\hspace{9mm}}l}
+ @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+ @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+ \end{array}}
+ \end{equation}
+ %
+ These cases lemmas have a premise for auch term-constructor.
+ The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
+ provided we can show that this property holds if we substitute for @{text "t"} all
+ possible term-constructors.
+
+ The only remaining difficulty is that in order to derive the stronger induction
+ principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that
+ in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and
+ \emph{all} @{text Let}-terms.
+ What we need instead is a cases rule where we only have to consider terms that have
+ binders being fresh w.r.t.~a context @{text "c"}, namely
+ %
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\
+ @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}
+ \end{tabular}
+ \end{center}
+ %
+ However, this can be relatively easily be derived from the implications in \eqref{weakcases}
+ by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know
+ that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with
+ a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and
+ @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold.
+ By using Property \ref{supppermeq}, we can infer that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"}
+ and we are done with this case.
+
+ The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated.
+ The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"},
+ because @{text p} might contain names that are bound (by @{text bn}) and that are
+ free. To solve this problem we have to introduce a permutation functions that only
+ permutes names bound by @{text bn} and leaves the other names unchanged. We do this again
+ by lifting. Assuming a
+ clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define
%
\begin{center}
@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}
\end{center}
-
+ %
\noindent
with @{text "y\<^isub>i"} determined as follows:
%
\begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}}
$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
\end{tabular}
\end{center}
+ %
+ Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that
+ @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
+ is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
+ these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
+ completes the interesting cases in \eqref{letpat} for stregthening the induction
+ principles.
- \noindent
- Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
- $\alpha$-equated terms. We can then prove the following two facts
+
- \begin{lemma}\label{permutebn}
- Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
- {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
- @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
- \end{lemma}
+ %A natural question is
+ %whether we can also strengthen the weak induction principles involving
+ %the general binders presented here. We will indeed be able to so, but for this we need an
+ %additional notion for permuting deep binders.
- \begin{proof}
- By induction on @{text x}. The equations follow by simple unfolding
- of the definitions.
- \end{proof}
+ %Given a binding function @{text "bn"} we define an auxiliary permutation
+ %operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
+ %Assuming a clause of @{text bn} is given as
+ %
+ %\begin{center}
+ %@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"},
+ %\end{center}
- \noindent
- The first property states that a permutation applied to a binding function is
- equivalent to first permuting the binders and then calculating the bound
- atoms. The second amounts to the fact that permuting the binders has no
- effect on the free-atom function. The main point of this permutation
- function, however, is that if we have a permutation that is fresh
- for the support of an object @{text x}, then we can use this permutation
- to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
- @{text "Let"} term-constructor from the example shown
- in \eqref{letpat} this means for a permutation @{text "r"}
+ %\noindent
+ %then we define
+ %
+ %\begin{center}
+ %@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"}
+ %\end{center}
+
+ %\noindent
+ %with @{text "y\<^isub>i"} determined as follows:
%
- \begin{equation}\label{renaming}
- \begin{array}{l}
- \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\
- \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
- \end{array}
- \end{equation}
+ %\begin{center}
+ %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+ %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+ %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+ %\end{tabular}
+ %\end{center}
+
+ %\noindent
+ %Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
+ %$\alpha$-equated terms. We can then prove the following two facts
+
+ %\begin{lemma}\label{permutebn}
+ %Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
+ %{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
+ % @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
+ %\end{lemma}
- \noindent
- This fact will be crucial when establishing the strong induction principles below.
+ %\begin{proof}
+ %By induction on @{text x}. The equations follow by simple unfolding
+ %of the definitions.
+ %\end{proof}
+
+ %\noindent
+ %The first property states that a permutation applied to a binding function is
+ %equivalent to first permuting the binders and then calculating the bound
+ %atoms. The second amounts to the fact that permuting the binders has no
+ %effect on the free-atom function. The main point of this permutation
+ %function, however, is that if we have a permutation that is fresh
+ %for the support of an object @{text x}, then we can use this permutation
+ %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the
+ %@{text "Let"} term-constructor from the example shown
+ %in \eqref{letpat} this means for a permutation @{text "r"}
+ %%
+ %\begin{equation}\label{renaming}
+ %\begin{array}{l}
+ %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\
+ %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}}
+ %\end{array}
+ %\end{equation}
+
+ %\noindent
+ %This fact will be crucial when establishing the strong induction principles below.
- In our running example about @{text "Let"}, the strong induction
- principle means that instead
- of establishing the implication
+ %In our running example about @{text "Let"}, the strong induction
+ %principle means that instead
+ %of establishing the implication
%
- \begin{center}
- @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
- \end{center}
-
- \noindent
- it is sufficient to establish the following implication
+ %\begin{center}
+ %@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
+ %\end{center}
+ %
+ %\noindent
+ %it is sufficient to establish the following implication
%
- \begin{equation}\label{strong}
- \mbox{\begin{tabular}{l}
- @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
- \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
- \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
- \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
- \end{tabular}}
- \end{equation}
-
- \noindent
- While this implication contains an additional argument, namely @{text c}, and
- also additional universal quantifications, it is usually easier to establish.
- The reason is that we have the freshness
- assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
- chosen by the user as long as it has finite support.
-
- Let us now show how we derive the strong induction principles from the
- weak ones. In case of the @{text "Let"}-example we derive by the weak
- induction the following two properties
+ %\begin{equation}\label{strong}
+ %\mbox{\begin{tabular}{l}
+ %@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+ %\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\
+ %\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
+ %\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
+ %\end{tabular}}
+ %\end{equation}
+ %
+ %\noindent
+ %While this implication contains an additional argument, namely @{text c}, and
+ %also additional universal quantifications, it is usually easier to establish.
+ %The reason is that we have the freshness
+ %assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily
+ %chosen by the user as long as it has finite support.
+ %
+ %Let us now show how we derive the strong induction principles from the
+ %weak ones. In case of the @{text "Let"}-example we derive by the weak
+ %induction the following two properties
+ %
+ %\begin{equation}\label{hyps}
+ %@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
+ %@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
+ %\end{equation}
%
- \begin{equation}\label{hyps}
- @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm}
- @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"}
- \end{equation}
-
- \noindent
- For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
- assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
- By Property~\ref{avoiding} we
- obtain a permutation @{text "r"} such that
+ %\noindent
+ %For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}
+ %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}).
+ %By Property~\ref{avoiding} we
+ %obtain a permutation @{text "r"} such that
%
- \begin{equation}\label{rprops}
- @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
- @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
- \end{equation}
-
- \noindent
- hold. The latter fact and \eqref{renaming} give us
+ %\begin{equation}\label{rprops}
+ %@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm}
+ %@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"}
+ %\end{equation}
+ %
+ %\noindent
+ %hold. The latter fact and \eqref{renaming} give us
+ %%
+ %\begin{center}
+ %\begin{tabular}{l}
+ %@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
+ %\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
+ %\end{tabular}
+ %\end{center}
%
- \begin{center}
- \begin{tabular}{l}
- @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\
- \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"}
- \end{tabular}
- \end{center}
-
- \noindent
- So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
- establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
- To do so, we will use the implication \eqref{strong} of the strong induction
- principle, which requires us to discharge
- the following four proof obligations:
+ %\noindent
+ %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
+ %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}.
+ %To do so, we will use the implication \eqref{strong} of the strong induction
+ %principle, which requires us to discharge
+ %the following four proof obligations:
+ %%
+ %\begin{center}
+ %\begin{tabular}{rl}
+ %{\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
+ %{\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
+ %{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
+ %{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
+ %\end{tabular}
+ %\end{center}
%
- \begin{center}
- \begin{tabular}{rl}
- {\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\
- {\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\
- {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\
- {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\
- \end{tabular}
- \end{center}
-
- \noindent
- The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
- others from the induction hypotheses in \eqref{hyps} (in the fourth case
- we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
-
- Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
- we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
- This completes the proof showing that the weak induction principles imply
- the strong induction principles.
+ %\noindent
+ %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the
+ %others from the induction hypotheses in \eqref{hyps} (in the fourth case
+ %we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}).
+ %
+ %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
+ %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
+ %This completes the proof showing that the weak induction principles imply
+ %the strong induction principles.
*}
@@ -2073,9 +2182,9 @@
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.
+ 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.
Another representation technique for binding is higher-order abstract syntax
(HOAS), which for example is implemented in the Twelf system. This representation
@@ -2158,9 +2267,10 @@
%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.
+ (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 in \cite{Pottier06} a language, called C$\alpha$ml, for
representing terms with general binders inside OCaml. This language is
@@ -2175,6 +2285,7 @@
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