--- a/Paper/Paper.thy	Thu Mar 18 16:22:10 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 18:43:03 2010 +0100
@@ -15,17 +15,131 @@
 section {* Introduction *}
 
 text {*
+  So far, Nominal Isabelle provided a mechanism to construct
+  automatically alpha-equated lambda terms sich as
 
-  It has not yet fared so well in the POPLmark challenge
-  as the second part contain a formalisation of records 
-  where ...
+  \begin{center}
+  $t ::= x \mid t\;t \mid \lambda x. t$
+  \end{center}
+
+  \noindent
+  For such calculi, it derived automatically a convenient reasoning
+  infrastructure. With this it has been used to formalise an equivalence
+  checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
+  Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
+  \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result
+  for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
+  used by Pollack for formalisations in the locally-nameless approach to
+  binding \cite{SatoPollack10}.
+
+  However, Nominal Isabelle has fared less well in a formalisation of
+  the algorithm W \cite{UrbanNipkow09} where types and type-schemes
+  are represented by
+
+  \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}
+
+  \noindent
+  While it is possible to formalise the finite set of variables that are
+  abstracted in a type-scheme by iterating single abstractions, it leads to a very
+  clumsy formalisation. This need of iterating single binders for representing
+  multiple binders is also the reason why Nominal Isabelle and other theorem
+  provers have so far not fared very well with the more advanced tasks in the POPLmark
+  challenge, because also there one would like to abstract several variables 
+  at once.
+
+  There are interesting points to note with binders that abstract multiple 
+  variables. First in the case of type-schemes we do not like to make a distinction
+  about the order of the binders. So 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}
+
+  \noindent
+  but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} 
+  alpha-equivalent:
+
+  \begin{center}
+  $\forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ 
+  \end{center}
+
+  \noindent
+  However we do 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}
 
-  The difficulty can be appreciated by considering that the
-  definition given by Leroy in \cite{Leroy92} is incorrect (it omits a
-  side-condition).
+  \noindent
+  In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence 
+  which can be used to represent type-schemes.  The difficulty in finding the notion of alpha-equivalence 
+  can be appreciated 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
+  alway wanted. For example in constructs like
+
+  \begin{center}
+  $\LET x = 3 \AND y = 2 \IN x \backslash y \END$
+  \end{center}
+
+  \noindent
+  we might not care in which order the associations $x = 3$ and $y = 2$ are
+  given, but it would be unusual to regard this term as alpha-equivalent with
+
+  \begin{center}
+  $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$
+  \end{center}
+
+  \noindent
+  We will provide a separate abstraction mechanism for this case where the
+  order of binders does not matter, but the ``cardinality'' of the binders
+  has to be the same.
+
+  However, this is still not sufficient for covering language constructs frequently 
+  occuring in programming language research. For example in patters like
 
-  Examples: type-schemes, Spi-calculus
+  \begin{center}
+  $\LET (x, y) = (3, 2) \IN x \backslash y \END$
+  \end{center}
+
+  \noindent
+  we want to bind all variables from the pattern (there might be an arbitrary
+  number of them) inside the body of the let, but we also care about the order
+  of these variables, since we do not want to identify this term with
+
+  \begin{center}
+  $\LET (y, x) = (3, 2) \IN x \backslash y \END$
+  \end{center}
+
+  \noindent
+  Therefore we have identified three abstraction mechanisms for multiple binders
+  and allow the user to chose which one is intended. 
 
+  By providing general abstraction mechanisms that allow the binding of multiple
+  variables, we have to work around aproblem that has been first pointed out
+  by Pottier in \cite{Pottier}: in let-constructs such as
+
+  \begin{center}
+  $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
+  \end{center}
+
+  \noindent
+  where the $x_i$ are bound in $s$. In this term we might not care about the order in 
+  which the $x_i = t_i$ are given, but we do care about the information that there are 
+  as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$
+  as something 
+
+  
+
+  
+  
   Contributions:  We provide definitions for when terms
   involving general bindings are alpha-equivelent.
 
@@ -129,6 +243,18 @@
 
 section {* Alpha-Equivalence and Free Variables *}
 
+text {*
+  Restrictions
+
+  \begin{itemize}
+  \item non-emptyness
+  \item positive datatype definitions
+  \item finitely supported abstractions
+  \item respectfulness of the bn-functions\bigskip
+  \item binders can only have a ``single scope''
+  \end{itemize}
+*}
+
 section {* Examples *}
 
 section {* Adequacy *}
@@ -138,6 +264,11 @@
 section {* Conclusion *}
 
 text {*
+  Complication when the single scopedness restriction is lifted (two 
+  overlapping permutations)
+*}
+
+text {*
 
   TODO: function definitions:
   \medskip

--- a/Paper/document/root.tex	Thu Mar 18 16:22:10 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 18:43:03 2010 +0100
@@ -16,6 +16,10 @@
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymiota}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\LET}{\;\mathtt{let}\;}
+\newcommand{\IN}{\;\mathtt{in}\;}
+\newcommand{\END}{\;\mathtt{end}\;}
+\newcommand{\AND}{\;\mathtt{and}\;}
 
 
 
@@ -41,12 +45,13 @@
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
 programming language calculi. In this paper we present an extension of Nominal
-Isabelle for dealing with general binding structures. Such binding structures are
-ubiquitous in programming language research and only very poorly handled by
-single binding from the lambda-calculus. We give in this
-paper novel definitions for alpha-equivalence and establish automatically the
-reasoning structure for alpha-equated terms. For example we provide a strong
-induction principle that has the variable convention already built in.
+Isabelle for dealing with general binding structures. Such binding structures
+are ubiquitous in programming language research and only very poorly supported
+by theorem provers providing only single binding as in the lambda-calculus. We
+give in this paper novel definitions for alpha-equivalence and establish
+automatically the reasoning structure for alpha-equated terms. For example we
+provide a strong induction principle that has the variable convention already
+built in.
 \end{abstract}