--- a/Paper/Paper.thy Mon Mar 22 10:21:14 2010 +0100
+++ b/Paper/Paper.thy Mon Mar 22 11:55:29 2010 +0100
@@ -57,25 +57,25 @@
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
-
- \begin{center}
- $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$
- \end{center}
+ %
+ \begin{equation}\label{ex1}
+ \forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x
+ \end{equation}
\noindent
but the following two should \emph{not} be alpha-equivalent
-
- \begin{center}
- $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$
- \end{center}
+ %
+ \begin{equation}\label{ex2}
+ \forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z
+ \end{equation}
\noindent
assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as
alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
-
- \begin{center}
- $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$
- \end{center}
+ %
+ \begin{equation}\label{ex3}
+ \forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y
+ \end{equation}
\noindent
where $z$ does not occur freely in the type.
@@ -268,7 +268,7 @@
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
- a resoning infrastructure needs to be ``lifted'' from the underlying subset to
+ 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
@@ -279,7 +279,7 @@
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 respectulness proofs which we automated.\medskip
+ lifting needs some respectfulness proofs which we automated.\medskip
\noindent
{\bf Contributions:} We provide new definitions for when terms
@@ -363,8 +363,8 @@
section {* General Binders *}
text {*
- In order to keep our work managable we give need to give definitions
- and perform proofs inside Isabelle whereever possible, as opposed to write
+ 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
@@ -378,45 +378,82 @@
in the body $x$ (similarly to type-schemes given in \eqref{tysch}).
The first question we have to answer is when we should consider pairs such as
- $(as, x)$ and $(bs, y)$ as alpha-equivelent? (At the moment we are interested in
+ $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in
the notion of alpha-equivalence that is \emph{not} preserved by adding
- vacuous binders.) For this we identify four conditions: i) given a free-variable function
- of type \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
- need to have the same set of free variables; ii) there must be a permutation,
- say $p$, that leaves the free variables $x$ and $y$ unchanged, but ``moves'' their bound names
- so that we obtain modulo a relation, say @{text "_ R _"},
- two equal terms. We also require that $p$ makes the abstracted sets equal. These
- requirements can be stated formally as
-
- \begin{center}
- \begin{tabular}{rcl}
- a
- \end{tabular}
- \end{center}
-
-
- Assuming we are given a free-variable function, say
- \mbox{@{text "fv :: \<beta> \<Rightarrow> atom set"}}, then we expect for two alpha-equivelent
- pairs that their sets of free variables aggree. That is
+ 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$
+ 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,
+ 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
%
- \begin{equation}\label{four}
- \mbox{@{text "(as, x) \<approx> (bs, y)"} \hspace{2mm}implies\hspace{2mm} @{text "fv(x) - as = fv(y) - bs"}}
+ \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]
+ & @{text "fv(x) - as = fv(y) - bs"}\\
+ \wedge & @{text "fv(x) - as #* p"}\\
+ \wedge & @{text "(p \<bullet> x) R y"}\\
+ \wedge & @{text "(p \<bullet> as) = bs"}\\
+ \end{array}
\end{equation}
\noindent
- Next we expect that there is a permutation, say $p$, that leaves the
- free variables unchanged, but ``moves'' the bound names in $x$ so that
- we obtain $y$ modulo a relation, say @{text "_ R _"}, that characterises when two
- elments of type $\beta$ are equivalent. We also expect that $p$
- makes the binders equal. We can formulate these requirements as: there
- exists a $p$ such that $i)$ @{term "(fv(x) - as) \<sharp>* p"}, $ii)$ @{text "(p \<bullet> x) R y"} and
- $iii)$ @{text "(p \<bullet> as) = bs"}.
+ 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$.
+
+ 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
+ %
+ \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]
+ & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
+ \wedge & @{text "fv(x) - (set as) #* p"}\\
+ \wedge & @{text "(p \<bullet> x) R y"}\\
+ \wedge & @{text "(p \<bullet> as) = bs"}\\
+ \end{array}
+ \end{equation}
+
+ \noindent
+ where $set$ is just the function that coerces a list of atoms into a set of atoms.
- We take now \eqref{four} and the three
-
+ 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
+ %
+ \begin{equation}\label{alphaset}
+ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
+ \multicolumn{2}{l}{(as, x) \approx_{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}
- General notion of alpha-equivalence (depends on a free-variable
- function and a relation).
+ 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{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.
*}
section {* Alpha-Equivalence and Free Variables *}
@@ -425,7 +462,7 @@
Restrictions
\begin{itemize}
- \item non-emptyness
+ \item non-emptiness
\item positive datatype definitions
\item finitely supported abstractions
\item respectfulness of the bn-functions\bigskip