--- a/Paper/Paper.thy	Mon Mar 22 11:55:29 2010 +0100
+++ b/Paper/Paper.thy	Mon Mar 22 16:22:07 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
@@ -467,6 +489,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 +526,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
+
+  
 *}
 
 

--- a/Paper/document/root.bib	Mon Mar 22 11:55:29 2010 +0100
+++ b/Paper/document/root.bib	Mon Mar 22 16:22:07 2010 +0100
@@ -81,6 +81,15 @@
   series = 	 {LNCS}
 }
 
+@article{MckinnaPollack99,
+  author =	 {J.~McKinna and R.~Pollack},
+  title =	 {{S}ome {T}ype {T}heory and {L}ambda {C}alculus {F}ormalised},
+  journal =	 {Journal of Automated Reasoning},
+  volume =       23,
+  number =       {1-4},
+  year =	 1999
+}
+
 @Unpublished{SatoPollack10,
   author = 	 {M.~Sato and R.~Pollack},
   title = 	 {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},