--- a/Paper/Paper.thy Mon Mar 22 18:29:29 2010 +0100
+++ b/Paper/Paper.thy Mon Mar 22 18:29:57 2010 +0100
@@ -53,8 +53,8 @@
more advanced tasks in the POPLmark challenge \cite{challenge05}, because
also there one would like to bind multiple variables at once.
- Binding multiple variables has interesting properties that are not captured
- by iterating single binders. For example in the case of type-schemes we do not
+ Binding multiple variables has interesting properties that cannot be captured
+ easily by iterating single binders. For example in the case of type-schemes we do not
like to make a distinction about the order of the bound variables. Therefore
we would like to regard the following two type-schemes as alpha-equivalent
%
@@ -152,7 +152,7 @@
would be a perfectly legal instance. To exclude such terms an additional
predicate about well-formed terms is needed in order to ensure that the two
lists are of equal length. This can result into very messy reasoning (see
- for example~\cite{BengtsonParow09}). To avoid this, we will allow specifications
+ for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
for $\mathtt{let}$s as follows
\begin{center}
@@ -165,7 +165,7 @@
\end{center}
\noindent
- where $assn$ is an auxiliary type representing a list of assignments
+ where $assn$ is an auxiliary type representing a list of assignments
and $bn$ an auxiliary function identifying the variables to be bound by
the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows
@@ -176,9 +176,9 @@
\noindent
The scope of the binding is indicated by labels given to the types, for
example \mbox{$s\!::\!trm$}, and a binding clause, in this case
- $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind all the names the function
- $bn$ returns in $s$. This style of specifying terms and bindings is heavily
- inspired by the syntax of the Ott-tool \cite{ott-jfp}.
+ $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the
+ function $bn\,(a)$ returns. This style of specifying terms and bindings is
+ heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}.
However, we will not be able to deal with all specifications that are
allowed by Ott. One reason is that Ott allows ``empty'' specifications
@@ -189,8 +189,8 @@
\end{center}
\noindent
- where no clause for variables is given. Such specifications make sense in
- the context of Coq's type theory (which Ott supports), but not in a HOL-based
+ where no clause for variables is given. Such specifications make some sense in
+ the context of Coq's type theory (which Ott supports), but not at al in a HOL-based
theorem prover where every datatype must have a non-empty set-theoretic model.
Another reason is that we establish the reasoning infrastructure
@@ -253,7 +253,7 @@
\end{center}
\noindent
- We take as the starting point a definition of raw terms (being defined as a
+ We take as the starting point a definition of raw terms (defined as a
datatype in Isabelle/HOL); identify then the
alpha-equivalence classes in the type of sets of raw terms, according to our
alpha-equivalence relation and finally define the new type as these
@@ -263,23 +263,45 @@
The fact that we obtain an isomorphism between between the new type and the non-empty
subset shows that the new type is a faithful representation of alpha-equated terms.
- That is different for example in the representation of terms using the locally
- nameless representation of binders: there are non-well-formed terms that need to
+ That is not the case for example in the representation of terms using the locally
+ nameless representation of binders \cite{McKinnaPollack99}: there are ``junk'' terms that need to
be excluded by reasoning about a well-formedness predicate.
- The problem with introducing a new type in Isabelle/HOL is that in order to be useful
+ The problem with introducing a new type in Isabelle/HOL is that in order to be useful,
a reasoning infrastructure needs to be ``lifted'' from the underlying subset to
the new type. This is usually a tricky and arduous task. To ease it
- we reimplemented in Isabelle/HOL the quotient package described by Homeier
- \cite{Homeier05}. Given that alpha is an equivalence relation, this package
- allows us to automatically lift definitions and theorems involving raw terms
- to definitions and theorems involving alpha-equated terms. This of course
- only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence.
- Hence we will be able to lift, for instance, the function for free
- variables of raw terms to alpha-equated terms (since this function respects
- alpha-equivalence), but we will not be able to do this with a bound-variable
- function (since it does not respect alpha-equivalence). As a result, each
- lifting needs some respectfulness proofs which we automated.\medskip
+ we re-implemented in Isabelle/HOL the quotient package described by Homeier
+ \cite{Homeier05}. This package
+ allows us to lift definitions and theorems involving raw terms
+ to definitions and theorems involving alpha-equated terms. For example
+ if we define the free-variable function over lambda terms
+
+ \begin{center}
+ $\fv(x) = \{x\}$\hspace{10mm}
+ $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]
+ $\fv(\lambda x.t) = \fv(t) - \{x\}$
+ \end{center}
+
+ \noindent
+ then with not too great effort we obtain a function $\fv_\alpha$
+ operating on quotients, or alpha-equivalence classes of terms, as follows
+
+ \begin{center}
+ $\fv_\alpha(x) = \{x\}$\hspace{10mm}
+ $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]
+ $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$
+ \end{center}
+
+ \noindent
+ (Note that this means also the term-constructors for variables, applications
+ and lambda are lifted to the quotient level.) This construction, of course,
+ only works if alpha is an equivalence relation, and the definitions and theorems
+ are respectful w.r.t.~alpha-equivalence. Hence we will not be able to lift this
+ a bound-variable function to alpha-equated terms (since it does not respect
+ alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness
+ properties. These proofs we are able automate and therefore establish a
+ useful reasoning infrastructure for alpha-equated lambda terms.\medskip
+
\noindent
{\bf Contributions:} We provide new definitions for when terms
@@ -363,36 +385,34 @@
section {* General Binders *}
text {*
- In order to keep our work manageable we give need to give definitions
- and perform proofs inside Isabelle wherever possible, as opposed to write
- custom ML-code that generates them for each
- instance of a term-calculus. To this end we will first consider pairs
+ In Nominal Isabelle the user is expected to write down a specification of a
+ term-calculus and a reasoning infrastructure is then automatically derived
+ from this specifcation (remember that Nominal Isabelle is a definitional
+ extension of Isabelle/HOL and cannot introduce new axioms).
+
- \begin{equation}\label{three}
- \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}
- \end{equation}
-
- \noindent
- consisting of a set of atoms and an object of generic type. These pairs
- are intended to represent the abstraction or binding of the set $as$
- in the body $x$ (similarly to type-schemes given in \eqref{tysch}).
+ In order to keep our work manageable, we will wherever possible state
+ definitions and perform proofs inside Isabelle, as opposed to write custom
+ ML-code that generates them for each instance of a term-calculus. To that
+ end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
+ These pairs are intended to represent the abstraction, or binding, of the set $as$
+ in the body $x$.
- The first question we have to answer is when we should consider pairs such as
- $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in
+ The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
+ alpha-equivalent? (At the moment we are interested in
the notion of alpha-equivalence that is \emph{not} preserved by adding
- vacuous binders.) To answer this we identify four conditions: {\it i)} given
- a free-variable function of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
+ vacuous binders.) To answer this, we identify four conditions: {\it i)} given
+ a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
need to have the same set of free variables; moreover there must be a permutation,
- $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged,
- but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
+ $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged,
+ but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes
- the abstracted sets $as$ and $bs$ equal (since at the moment we do not want
- that the sets $as$ and $bs$ differ on vacuous binders). These requirements can
- be stated formally as follows
+ the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can
+ be stated formally as follows:
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{(as, x) \approx_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+ \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - as = fv(y) - bs"}\\
\wedge & @{text "fv(x) - as #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
@@ -401,20 +421,23 @@
\end{equation}
\noindent
- Alpha equivalence between such pairs is then the relation with the additional
- existential quantification over $p$. Note that this relation is additionally
- dependent on the free-variable function $\fv$ and the relation $R$. The reason
- for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms
- and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and
- we are going to prove that $\fv$ will be equal to the support of $x$ and $y$.
+ Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where
+ we existentially quantify over this $p$.
+ Also note that the relation is dependent on a free-variable function $\fv$ and a relation
+ $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both
+ ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by
+ equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support
+ of $x$ and $y$. To have these parameters means, however, we can derive properties about
+ them generically.
The definition in \eqref{alphaset} does not make any distinction between the
- order of abstracted variables. If we do want this then we can define alpha-equivalence
- for pairs of the form \mbox{@{text "(as, x) :: (atom list) \<times> \<beta>"}} by
+ order of abstracted variables. If we want this, then we can define alpha-equivalence
+ for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
+ as follows
%
\begin{equation}\label{alphalist}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+ \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
\wedge & @{text "fv(x) - (set as) #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
@@ -426,34 +449,65 @@
where $set$ is just the function that coerces a list of atoms into a set of atoms.
If we do not want to make any difference between the order of binders and
- allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset}
- and define
+ also allow vacuous binders, then we keep sets of binders, but drop the fourth
+ condition in \eqref{alphaset}:
%
- \begin{equation}\label{alphaset}
+ \begin{equation}\label{alphares}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
+ \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - as = fv(y) - bs"}\\
\wedge & @{text "fv(x) - as #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
\end{array}
\end{equation}
- To get a feeling how these definitions pan out in practise consider the case of
- abstracting names over types (like in type-schemes). For this we set $R$ to be
- the equality and for $\fv(T)$ we define
+ \begin{exmple}\rm
+ It might be useful to consider some examples for how these definitions pan out in practise.
+ For this consider the case of abstracting a set of variables over types (as in type-schemes).
+ We set $R$ to be the equality and for $\fv(T)$ we define
\begin{center}
$\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$
\end{center}
\noindent
- Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily
- checked that @{text "({x,y}, x \<rightarrow> y)"} and
- @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to
- be the swapping @{text "(x \<rightleftharpoons> y)"}; but assuming @{text "x \<noteq> y"} then for instance
- $([x,y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
- makes the lists @{text "[x,y]"} and @{text "[y,x]"} equal, but leaves the type \mbox{@{text "x \<rightarrow> y"}}
- unchanged.
+ Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily
+ checked that @{text "({x, y}, x \<rightarrow> y)"} and
+ @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
+ be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then
+ $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
+ makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the
+ type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
+ $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
+ However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
+ the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
+ \end{exmple}
+
+ \noindent
+ Let $\star$ range over $\{set, res, list\}$. We prove next under which
+ conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence
+ relations and equivariant:
+
+ \begin{lemma}
+ {\it i)} Given the fact that $x\;R\;x$ holds, then
+ $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given
+ that @{text "(p \<bullet> x) R y"} implies @{text "(-p \<bullet> y) R x"}, then
+ $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies
+ $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given
+ that @{text "(p \<bullet> x) R y"} and @{text "(q \<bullet> y) R z"} implies
+ @{text "((q + p) \<bullet> x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$
+ and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies
+ $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given
+ @{text "(q \<bullet> x) R y"} implies @{text "(p \<bullet> (q \<bullet> x)) R (p \<bullet> y)"} and
+ @{text "p \<bullet> (fv x) = fv (p \<bullet> x)"} then @{text "p \<bullet> (fv y) = fv (p \<bullet> y)"}, then
+ $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies
+ $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star
+ (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$.
+ \end{lemma}
+
+ \begin{proof}
+ All properties are by unfolding the definitions and simple calculations.
+ \end{proof}
*}
section {* Alpha-Equivalence and Free Variables *}
@@ -467,6 +521,7 @@
\item finitely supported abstractions
\item respectfulness of the bn-functions\bigskip
\item binders can only have a ``single scope''
+ \item all bindings must have the same mode
\end{itemize}
*}
@@ -503,7 +558,11 @@
also for patiently explaining some of the finer points about the abstract
definitions and about the implementation of the Ott-tool.
+ Lookup: Merlin paper by James Cheney; Mark Shinwell PhD
+ Future work: distinct list abstraction
+
+
*}