
diff -r b39108f42638 -r 69c9d53fb817 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Mar 22 14:07:07 2010 +0100
+++ b/Paper/Paper.thy	Mon Mar 22 14:07:35 2010 +0100
@@ -36,12 +36,12 @@
   However, Nominal Isabelle has fared less well in a formalisation of
   the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
   are of the form
-
-  \begin{center}
-  \begin{tabular}{l}
-  $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$
-  \end{tabular}
-  \end{center}
+  %
+  \begin{equation}\label{tysch}
+  \begin{array}{l}
+  T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T
+  \end{array}
+  \end{equation}
 
   \noindent
   and the quantification $\forall$ binds a finite (possibly empty) set of
@@ -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.
@@ -157,9 +157,9 @@
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
-  $trm$ & $=$  & \ldots\\ 
+  $trm$ & $::=$  & \ldots\\ 
         & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm]
-  $assn$ & $=$  & $\mathtt{anil}$\\
+  $assn$ & $::=$  & $\mathtt{anil}$\\
          & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$
   \end{tabular}
   \end{center}
@@ -181,9 +181,21 @@
   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 we establish the reasoning infrastructure
-  for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of
-  its specifications a reasoning infrastructure in Isabelle/HOL for
+  allowed by Ott. One reason is that Ott allows ``empty'' specifications
+  like
+
+  \begin{center}
+  $t ::= t\;t \mid \lambda x. t$
+  \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 
+  theorem prover where every datatype must have a non-empty set-theoretic model.
+
+  Another reason is that we establish the reasoning infrastructure
+  for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning 
+  infrastructure in Isabelle/HOL for
   \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
   and the raw terms produced by Ott use names for bound variables,
   there is a key difference: working with alpha-equated terms means that the
@@ -247,7 +259,7 @@
   alpha-equivalence relation and finally define the new type as these 
   alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are 
   definable as datatype in Isabelle/HOL and the fact that our relation for alpha is an 
-  equivalence relation).\marginpar{\footnotesize Does Ott allow definitions of ``strange'' types?}
+  equivalence relation).
 
   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. 
@@ -255,11 +267,11 @@
   nameless representation of binders: there are non-well-formed terms that need to
   be excluded by reasoning about a well-formedness predicate.
 
-  The problem with introducing a new type is that in order to be useful 
-  a resoning infrastructure needs to be ``lifted'' from the underlying type
-  and subset to the new type. This is usually a tricky task. To ease this task 
+  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}. Gieven that alpha is an equivalence relation, this package 
+  \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.
@@ -267,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
@@ -287,11 +299,11 @@
   Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in
   \cite{HuffmanUrban10}, which we review here briefly to aid the description
   of what follows. Two central notions in the nominal logic work are sorted
-  atoms and permutations of atoms. The sorted atoms represent different kinds
-  of variables, such as term- and type-variables in Core-Haskell, and it is
-  assumed that there is an infinite supply of atoms for each sort. However, in
-  order to simplify the description, we shall assume in what follows that
-  there is only a single sort of atoms.
+  atoms and sort-respecting permutations of atoms. The sorts can be used to
+  represent different kinds of variables, such as term- and type-variables in
+  Core-Haskell, and it is assumed that there is an infinite supply of atoms
+  for each sort. However, in order to simplify the description, we shall
+  assume in what follows that there is only a single sort of atoms.
 
 
   Permutations are bijective functions from atoms to atoms that are 
@@ -302,19 +314,20 @@
 
   \noindent 
   with a generic type in which @{text "\<alpha>"} stands for the type of atoms 
-  and @{text "\<beta>"} for the type of the objects on which the permutation 
+  and @{text "\<beta>"} for the type of the object on 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"}} 
-  and the inverse permutation @{term p} as @{text "- p"}. The permutation
+  and the inverse permutation of @{term p} as @{text "- p"}. The permutation
   operation is defined for products, lists, sets, functions, booleans etc 
   (see \cite{HuffmanUrban10}).
 
-  The most original aspect of the nominal logic work of Pitts et al is a general
-  definition for ``the set of free variables of an object @{text "x"}''.  This
-  definition is general in the sense that it applies not only to lambda-terms,
-  but also to lists, products, sets and even functions. The definition depends
-  only on the permutation operation and on the notion of equality defined for
-  the type of @{text x}, namely:
+  The most original aspect of the nominal logic work of Pitts is a general
+  definition for the notion of ``the set of free variables of an object @{text
+  "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
+  it applies not only to lambda-terms alpha-equated or not, but also to lists,
+  products, sets and even functions. The definition depends only on the
+  permutation operation and on the notion of equality defined for the type of
+  @{text x}, namely:
 
   @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
 
@@ -350,54 +363,97 @@
 section {* General Binders *}
 
 text {*
-  In order to keep our work managable we like to state general definitions  
-  and perform proofs inside Isabelle as much as possible, as opposed to write
-  custom ML-code that generates appropriate definitions and proofs for each 
-  instance of a term-calculus. For this, we like to consider pairs
+  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
 
   \begin{equation}\label{three}
-  \mbox{@{text "(as, x) :: atom set \<times> \<beta>"}}
+  \mbox{@{text "(as, x) :: (atom set) \<times> \<beta>"}}
   \end{equation}
  
   \noindent
-  consisting of a set of atoms and an object of generic type. The pairs
-  are intended to be used for representing binding such as found in 
-  type-schemes
+  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}). 
 
-  \begin{center}
-  $\forall \{x_1,\ldots,x_n\}. T$
-  \end{center}
-  
-  \noindent
-  where the atoms $x_1,\ldots,x_n$ is intended to be in \eqref{three} the 
-  set @{text as} of atoms we want to bind, and $T$, an object-level type, is 
-  one instance for the generic $x$.
-
-  The first question we have to answer is when we should consider the pairs 
-  in \eqref{three} as alpha-equivelent? (At the moment we are interested in
+  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 notion of alpha-equivalence that is \emph{not} preserved by adding 
-  vacuous binders.) 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 *}
@@ -406,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
@@ -420,6 +476,14 @@
 
 section {* Related Work *}
 
+text {*
+  Ott is better with list dot specifications; subgrammars
+
+  untyped; 
+  
+*}
+
+
 section {* Conclusion *}
 
 text {*




