
diff -r 029f8aabed12 -r 5dc48e1af733 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue May 18 14:40:05 2010 +0100
+++ b/Paper/Paper.thy	Wed May 19 12:43:38 2010 +0100
@@ -9,7 +9,7 @@
   alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
   Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
-  
+  Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 
 
 definition
  "equal \<equiv> (op =)" 
@@ -33,6 +33,7 @@
   Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
   Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and
   Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
+  Abs_print ("_\<^raw:$\!$>\<^bsub>set\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
   supp_gen ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
@@ -52,15 +53,15 @@
   \end{center}
 
   \noindent
-  where free and bound variables have names.  For such alpha-equated terms,  Nominal Isabelle
-  derives automatically a reasoning infrastructure that has been used
-  successfully in formalisations of an equivalence checking algorithm for LF
-  \cite{UrbanCheneyBerghofer08}, Typed
+  where free and bound variables have names.  For such alpha-equated terms,
+  Nominal Isabelle derives automatically a reasoning infrastructure that has
+  been used successfully in formalisations of an equivalence checking
+  algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
   Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-  \cite{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}.
+  \cite{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,
@@ -546,7 +547,7 @@
 
   \noindent or equivalently that a permutation applied to the application
   @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-  functions @{text f} we have for all permutations @{text p}
+  functions @{text f}, we have for all permutations @{text p}
   %
   \begin{equation}\label{equivariance}
   @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
@@ -798,7 +799,8 @@
   \end{proof}
 
   \noindent
-  This lemma together with \eqref{absperm} allows us to show
+  Assuming that @{text "x"} has finite support, this lemma together 
+  with \eqref{absperm} allows us to show
   %
   \begin{equation}\label{halfone}
   @{thm abs_supports(1)[no_vars]}
@@ -918,11 +920,10 @@
   the second is for sets of binders (the order does not matter, but the
   cardinality does) and the last is for sets of binders (with vacuous binders
   preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding
-  clause will be called \emph{bodies} (there can be more than one); the 
-  ``\isacommand{bind}-part'' will be called \emph{binders}. 
-
-  In contrast to Ott, we allow multiple labels in binders and bodies. For example
-  we allow binding clauses of the form:
+  clause will be called \emph{bodies} (there can be more than one); the
+  ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
+  Ott, we allow multiple labels in binders and bodies. For example we allow
+  binding clauses of the form:
 
   \begin{center}
   \begin{tabular}{@ {}ll@ {}}
@@ -936,8 +937,9 @@
 
   \noindent
   Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
-  and \isacommand{bind\_res} the binding clauses will make a difference in
-  terms of the corresponding alpha-equivalence. We will show this later with an example.
+  and \isacommand{bind\_res} the binding clauses will make a difference to the semantics
+  of the specification (the corresponding alpha-equivalence will differ). We will 
+  show this later with an example.
   
   There are some restrictions we need to impose: First, a body can only occur
   in \emph{one} binding clause of a term constructor. For binders we
@@ -972,8 +974,8 @@
   \noindent
   Note that for @{text lam} it does not matter which binding mode we use. The
   reason is that we bind only a single @{text name}. However, having
-  \isacommand{bind\_set} or \isacommand{bind} in the second case again makes a
-  difference to the underlying notion of alpha-equivalence. Note also that in
+  \isacommand{bind\_set} or \isacommand{bind} in the second case makes again a
+  difference to the semantics of the specification. Note also that in
   these specifications @{text "name"} refers to an atom type, and @{text
   "fset"} to the type of finite sets.
 
@@ -1032,7 +1034,7 @@
   binders \emph{recursive}.  To see the purpose of such recursive binders,
   compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
   specification:
-  %
+
   \begin{equation}\label{letrecs}
   \mbox{%
   \begin{tabular}{@ {}l@ {}}
@@ -1055,11 +1057,10 @@
   The difference is that with @{text Let} we only want to bind the atoms @{text
   "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
   inside the assignment. This difference has consequences for the free-variable 
-  function and alpha-equivalence relation, which we are going to describe in the 
-  rest of this section.
+  function and alpha-equivalence relation, which we are going to define below.
   
-  The restriction we have to impose on deep binders is that we cannot have
-  more than one binding function for one binder. So we exclude:
+  For this definition, we have to impose some restrictions on deep binders. First,
+  we cannot have more than one binding function for one binder. So we exclude:
 
   \begin{center}
   \begin{tabular}{ll}
@@ -1090,8 +1091,8 @@
   In order to simplify our definitions, we shall assume specifications 
   of term-calculi are \emph{completed}. By this we mean that  
   for every argument of a term-constructor that is \emph{not} 
-  already part of a binding clause, we add implicitly a special \emph{empty} binding
-  clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "label"}. In case
+  already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
+  clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
   of the lambda-calculus, the completion produces
 
   \begin{center}
@@ -1100,8 +1101,7 @@
   \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
     \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\
   \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"}
-    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1"},
-        \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\
+    \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
     \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
   \end{tabular}
@@ -1913,13 +1913,13 @@
   approach to binding \cite{chargueraud09}.  There, 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
-  representations of bindings comes for free in the theorem provers, like Isabelle/HOL or
+  representations of bindings comes for free in theorem provers like Isabelle/HOL or
   Coq, 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, one would require additional predicates that filter out
-  unwanted terms. Our guess is that such predicates results in rather
+  unwanted terms. Our guess is that such predicates result in rather
   intricate formal reasoning.
 
   Another representation technique for binding is higher-order abstract syntax
@@ -1936,39 +1936,93 @@
   all the unwanted consequences when reasoning about the resulting terms.
 
   Two formalisations involving general binders have also been performed in older
-  versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}.  Both
+  versions of Nominal Isabelle (one about Psi-calculi and one about alpgorithm W 
+  \cite{BengtsonParow09, UrbanNipkow09}).  Both
   use the approach based on iterated single binders. Our experience with
   the latter formalisation has been disappointing. The major pain arose 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
+  general binders, but needs a cumbersome
   iteration with single binders. The resulting formal reasoning turned out to
   be rather unpleasant. The hope is that the extension presented in this paper
   is a substantial improvement.
  
-  The most closely related work to the one presented here is the Ott-tool \cite{ott-jfp}. This tool is a
-  nifty front-end for creating \LaTeX{} documents from specifications of
-  term-calculi involving general binders. For a subset of the specifications, Ott can also generate
-  theorem prover code using a raw representation of terms, and in Coq also a
-  locally nameless representation. The developers of this tool have also put
-  forward (on paper) a definition for alpha-equivalence of terms that can be
-  specified in Ott.  This definition is rather different from ours, not using
-  any nominal techniques. Although we were heavily inspired by their syntax,
+  The most closely related work to the one presented here is the Ott-tool
+  \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
+  front-end for creating \LaTeX{} documents from specifications of
+  term-calculi involving general binders. For a subset of the specifications,
+  Ott can also generate theorem prover code using a raw representation of
+  terms, and in Coq also a locally nameless representation. The developers of
+  this tool have also put forward (on paper) a definition for
+  alpha-equivalence of terms that can be specified in Ott.  This definition is
+  rather different from ours, not using any nominal techniques.  To our
+  knowledge there is also no concrete mathematical result concerning this
+  notion of alpha-equivalence.  A definition for the notion of free variables
+  in a term are work in progress in Ott.
+
+  Although we were heavily inspired by their syntax,
   their definition of alpha-equivalence is unsuitable 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. Third, it allows empty types that have no
-  meaning in a HOL-based theorem prover.
+  meaning in a HOL-based theorem prover. We also had to generalise slightly their 
+  binding clauses. In Ott you specify binding clauses with a single body; we 
+  allow more than one. We have to do this, because this makes a difference 
+  for our notion of alpha-equivalence in case of \isacommand{bind\_set} and 
+  \isacommand{bind\_res}. This makes 
+
+  \begin{center}
+  \begin{tabular}{@ {}ll@ {}}
+  @{text "Foo\<^isub>1 xs::name fset x::name y::name"} &  
+      \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "x y"}\\
+  @{text "Foo\<^isub>2 xs::name fset x::name y::name"} &  
+      \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "x"}, 
+      \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "y"}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  behave differently. To see this, consider the following equations 
+
+  \begin{center}
+  \begin{tabular}{c}
+  @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (b, a)"}\\
+  @{term "Abs_print [a,b] (a, b) = Abs_print [a,b] (a, b)"}\\
+  \end{tabular}
+  \end{center}
+  
+  \noindent
+  The interesting point is that they do not imply
+
+   \begin{center}
+  \begin{tabular}{c}
+  @{term "Abs_print [a,b] ((a, b), (a, b)) = Abs_print [a,b] ((a, b), (b, a))"}\\
+  \end{tabular}
+  \end{center}
 
   Because of how we set up our definitions, we had to impose restrictions,
-  like excluding overlapping deep binders, that are not present in Ott. Our
+  like a single binding function for a deep binder, that are not present in Ott. Our
   expectation is that we can still cover many interesting term-calculi from
   programming language research, for example Core-Haskell. For providing support
   of neat features in Ott, such as subgrammars, the existing datatype
   infrastructure in Isabelle/HOL is unfortunately not powerful enough. On the
   other hand, we are not aware that Ott can make the distinction between our
-  three different binding modes. Also, definitions for notions like the free
-  variables of a term are work in progress in Ott.
+  three different binding modes.
+
+  Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for 
+  representing terms with general binders inside OCaml. This language is
+  implemented as a front-end that can be translated to OCaml with a help of
+  a library. He presents a type-system in which the scope of general binders
+  can be indicated with some special constructs, written @{text "inner"} and 
+  @{text "outer"}. With this, it seems, our and his specifications can be
+  inter-translated, but we have not proved this. However, we believe the
+  binding specifications in the style of Ott are a more natural way for 
+  representing terms involving bindings. Pottier gives a definition for 
+  alpha-equivalence, which is similar to our binding mod \isacommand{bind}. 
+  Although he uses also a permutation in case of abstractions, his
+  definition is rather different from ours. He proves that his notion
+  of alpha-equivalence is indeed a equivalence relation, but a complete
+  reasoning infrastructure is well beyond the purposes of his language. 
 *}
 
 section {* Conclusion *}
@@ -2002,45 +2056,7 @@
   version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For
   them we need a more clever implementation than we have at the moment. 
 
-  More
-  interesting is lifting our restriction about overlapping deep binders. Given
-  our current setup, we cannot deal with specifications such as
-
- 
-  \begin{center}
-  \begin{tabular}{ll}
-  @{text "Foo r::pat s::pat t::trm"} & 
-     \isacommand{bind} @{text "bn(r)"} \isacommand{in} @{text t},\;
-     \isacommand{bind} @{text "bn(s)"} \isacommand{in} @{text t}
-  \end{tabular}
-  \end{center}
-  
-  \noindent
-  where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap. 
-  The difficulty is that we would need to implement such overlapping bindings 
-  with alpha-equivalences like
-
-  \begin{center}
-  @{term "\<exists>p q. abs_set2 (bn r\<^isub>1, t\<^isub>1) p (bn r\<^isub>2, t\<^isub>2) \<and> abs_set2 (bn s\<^isub>1, t\<^isub>1) q (bn s\<^isub>2, t\<^isub>2)"}
-  \end{center}
-
-  \noindent
-  or
-
-  \begin{center}
-  @{term "\<exists>p q. abs_set2 (bn r\<^isub>1 \<union> bn s\<^isub>1, t\<^isub>1) (p + q)  (bn r\<^isub>2 \<union> bn s\<^isub>2, t\<^isub>2)"}
-  \end{center}
-
-  \noindent
-  Both versions require two permutations (for each binding). But unfortunately the 
-  first version cannot work since it leaves some atoms unbound that should be 
-  bound by the respective other binder. This problem is avoided in the second
-  version, but at the expense that the two permutations can interfere with each 
-  other. We have not yet been able to find a way to avoid such interferences. 
-  On the other hand, such bindings can be made sense of informally \cite{SewellBestiary}.
-  This suggest there should be an approriate notion of alpha-equivalence.
-
-  Another interesting line of investigation is whether we can go beyond the 
+  More interesting line of investigation is whether we can go beyond the 
   simple-minded form for binding functions that we adopted from Ott. At the moment, binding
   functions can only return the empty set, a singleton atom set or unions
   of atom sets (similarly for lists). It remains to be seen whether 




