--- a/Paper/Paper.thy	Thu Apr 01 03:28:28 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 05:40:12 2010 +0200
@@ -1720,53 +1720,69 @@
 section {* Related Work *}
 
 text {*
-  To our knowledge the earliest usage of general binders in a theorem prover setting is 
-  in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of 
-  the algorithm W. This formalisation implements binding in type schemes using a 
-  a de-Bruijn indices representation. Also recently an extension for general binders 
-  has been proposed for the locally nameless approach to binding \cite{chargueraud09}. .
-  But we have not yet seen it to be employed in a non-trivial formal verification.
-  In both approaches, it seems difficult to achieve our fine-grained control over the
-  ``semantics'' of bindings (whether the order should matter, or vacous binders 
-  should be taken into account). To do so, it is necessary to introduce predicates 
-  that filter out some unwanted terms. This very likely results in intricate 
-  formal reasoning.
+  To our knowledge the earliest usage of general binders in a theorem prover
+  setting is in \cite{NaraschewskiNipkow99}, which describes a formalisation
+  of the algorithm W. This formalisation implements binding in type schemes
+  using a de-Bruijn indices representation. Since type schemes contain only a
+  single binder, different indices do not refer to different binders (as in
+  the usual de-Bruijn representation), but to different bound variables. Also
+  recently an extension for general binders has been proposed for the locally
+  nameless approach to binding \cite{chargueraud09}.  In this proposal, de-Bruijn 
+  indices consist of two numbers, one referring to the place where a variable is bound
+  and the other to which variable is bound. The reasoning infrastructure for both
+  kinds of de-Bruijn indices comes for free in any modern theorem prover as
+  the corresponding term-calculi can be implemented as ``normal'' datatypes.
+  However, in both approaches, it seems difficult to achieve our fine-grained
+  control over the ``semantics'' of bindings (i.e.~whether the order of
+  binders should matter, or vacuous binders should be taken into account). To
+  do so, requires additional predicates that filter out some unwanted
+  terms. Our guess is that they results in rather intricate formal reasoning.
+
+  Another representation technique for binding is higher-order abstract syntax
+  (HOAS), for example implemented in the Twelf system. This representation
+  technique supports very elegantly some aspects of \emph{single} binding, and
+  impressive work is in progress that uses HOAS for mechanising the metatheory
+  of SML \cite{LeeCraryHarper07}. We are not aware how multiple binders of SML
+  are represented in this work, but the submitted Twelf-solution for the
+  POPLmark challenge reveals that HOAS cannot easily deal with binding
+  constructs where the number of bound variables is not fixed. For example in
+  the second part of this challenge, @{text "Let"}s involve patterns and bind
+  multiple variables at once. In such situations, HOAS needs to use, essentially,
+  iterated single binders for representing multiple binders.
+
+  Two formalisations involving general binders have been performed in older
+  versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}.  Both
+  use the approach based on iterated single binders. Our experience with the
+  latter formalisation has been far from satisfying. The major pain arises
+  from the need to ``unbind'' variables. This can be done in one step with our
+  general binders, for example @{term "Abs as x"}, but needs a cumbersome
+  iteration with single binders. The resulting formal reasoning is rather
+  unpleasant. The hope is that the extension presented in this paper is a
+  substantial improvement.  
  
-  Higher-Order Abstract Syntax (HOAS) approaches to representing binders are
-  nicely supported in the Twelf theorem prover and work is in progress to use
-  HOAS in a mechanisation of the metatheory of SML
-  \cite{LeeCraryHarper07}. HOAS supports elegantly reasoning about
-  term-calculi with single binders. We are not aware how more complicated
-  binders from SML are represented in HOAS, but we know that HOAS cannot
-  easily deal with binding constructs where the number of bound variables is
-  not fixed. An example is the second part of the POPLmark challenge where
-  @{text "Let"}s involving patterns need to be formalised. In such situations
-  HOAS needs to use essentially has to represent multiple binders with
-  iterated single binders.
-
-  An attempt of representing general binders in the old version of Isabelle 
-  based also on iterating single binders is described in \cite{BengtsonParow09}. 
-  The reasoning there turned out to be quite complex. 
-
-  Ott is better with list dot specifications; subgrammars, is untyped; 
+  The most closely related work is the description of the Ott-tool
+  \cite{ott-jfp}. This tool is a nifty front end for creating \LaTeX{}
+  documents from term-calculi specifications. For a subset of the specifications,
+  Ott can also generate theorem prover code using a raw representation and
+  a locally nameless representation for terms. The developers of this tool
+  have also put forward a definition for the notion of
+  alpha-equivalence of the term-calculi that can be specified in Ott.  This
+  definition is rather different from ours, not using any of the nominal 
+  techniques; it also aims for maximum expressivity, covering
+  as many binding structures from programming language research as possible.
+  Although we were heavily inspired by their syntax, their definition of 
+  alpha-equivalence was no use at all for our extension of Nominal Isabelle. 
+  First, it is far too complicated to be a basis for automated proofs 
+  implemented on the ML-level of Isabelle/HOL. Second, it covers cases of 
+  binders depending on other binders, which just do not make sense for 
+  our alpha-equated terms, and it also allows empty types that have no meaning 
+  in a HOL-based theorem prover. For features of Ott, like subgrammars, the
+  datatype infrastructure in Isabelle/HOL is unfortunately not powerful 
+  enough. On the other hand we are not aware that Ott can make any distinction
+  between our three different binding modes. Also, definitions for notions like 
+  free-variables are work in progress in Ott.
 *}
 
-text {*
-%%% FIXME: The restricions should have already been described in previous sections?
-  Restrictions
-
-  \begin{itemize}
-  \item non-emptiness
-  \item positive datatype definitions
-  \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}
-*}
-  
-
-
 section {* Conclusion *}
 
 text {*
@@ -1777,7 +1793,6 @@
 
   TODO: function definitions:
   
-
   The formalisation presented here will eventually become part of the 
   Isabelle distribution, but for the moment it can be downloaded from 
   the Mercurial repository linked at 
@@ -1794,7 +1809,19 @@
   of kinds and types in our Core-Haskell example.  
 *}
 
+text {*
+%%% FIXME: The restricions should have already been described in previous sections?
+  Restrictions
 
+  \begin{itemize}
+  \item non-emptiness
+  \item positive datatype definitions
+  \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}
+*}
 
 (*<*)
 end