1723   To our knowledge the earliest usage of general binders in a theorem prover setting is 

  1723   To our knowledge the earliest usage of general binders in a theorem prover

  1724   in the paper \cite{NaraschewskiNipkow99}, which describes a formalisation of 

  1724   setting is in \cite{NaraschewskiNipkow99}, which describes a formalisation

  1725   the algorithm W. This formalisation implements binding in type schemes using a 

  1725   of the algorithm W. This formalisation implements binding in type schemes

  1726   a de-Bruijn indices representation. Also recently an extension for general binders 

  1726   using a de-Bruijn indices representation. Since type schemes contain only a

  1727   has been proposed for the locally nameless approach to binding \cite{chargueraud09}. .

  1727   single binder, different indices do not refer to different binders (as in

  1728   But we have not yet seen it to be employed in a non-trivial formal verification.

  1728   the usual de-Bruijn representation), but to different bound variables. Also

  1729   In both approaches, it seems difficult to achieve our fine-grained control over the

  1729   recently an extension for general binders has been proposed for the locally

  1730   ``semantics'' of bindings (whether the order should matter, or vacous binders 

  1730   nameless approach to binding \cite{chargueraud09}.  In this proposal, de-Bruijn 

  1731   should be taken into account). To do so, it is necessary to introduce predicates 

  1731   indices consist of two numbers, one referring to the place where a variable is bound

  1732   that filter out some unwanted terms. This very likely results in intricate 

  1732   and the other to which variable is bound. The reasoning infrastructure for both

  1733   formal reasoning.

  1733   kinds of de-Bruijn indices comes for free in any modern theorem prover as

  1734   the corresponding term-calculi can be implemented as ``normal'' datatypes.

  1735   However, in both approaches, it seems difficult to achieve our fine-grained

  1736   control over the ``semantics'' of bindings (i.e.~whether the order of

  1737   binders should matter, or vacuous binders should be taken into account). To

  1738   do so, requires additional predicates that filter out some unwanted

  1739   terms. Our guess is that they results in rather intricate formal reasoning.

  1740 

  1741   Another representation technique for binding is higher-order abstract syntax

  1742   (HOAS), for example implemented in the Twelf system. This representation

  1743   technique supports very elegantly some aspects of \emph{single} binding, and

  1744   impressive work is in progress that uses HOAS for mechanising the metatheory

  1745   of SML \cite{LeeCraryHarper07}. We are not aware how multiple binders of SML

  1746   are represented in this work, but the submitted Twelf-solution for the

  1747   POPLmark challenge reveals that HOAS cannot easily deal with binding

  1748   constructs where the number of bound variables is not fixed. For example in

  1749   the second part of this challenge, @{text "Let"}s involve patterns and bind

  1750   multiple variables at once. In such situations, HOAS needs to use, essentially,

  1751   iterated single binders for representing multiple binders.

  1752 

  1753   Two formalisations involving general binders have been performed in older

  1754   versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}.  Both

  1755   use the approach based on iterated single binders. Our experience with the

  1756   latter formalisation has been far from satisfying. The major pain arises

  1757   from the need to ``unbind'' variables. This can be done in one step with our

  1758   general binders, for example @{term "Abs as x"}, but needs a cumbersome

  1759   iteration with single binders. The resulting formal reasoning is rather

  1760   unpleasant. The hope is that the extension presented in this paper is a

  1761   substantial improvement.  

  1735   Higher-Order Abstract Syntax (HOAS) approaches to representing binders are

  1763   The most closely related work is the description of the Ott-tool

  1736   nicely supported in the Twelf theorem prover and work is in progress to use

  1764   \cite{ott-jfp}. This tool is a nifty front end for creating \LaTeX{}

  1737   HOAS in a mechanisation of the metatheory of SML

  1765   documents from term-calculi specifications. For a subset of the specifications,

  1738   \cite{LeeCraryHarper07}. HOAS supports elegantly reasoning about

  1766   Ott can also generate theorem prover code using a raw representation and

  1739   term-calculi with single binders. We are not aware how more complicated

  1767   a locally nameless representation for terms. The developers of this tool

  1740   binders from SML are represented in HOAS, but we know that HOAS cannot

  1768   have also put forward a definition for the notion of

  1741   easily deal with binding constructs where the number of bound variables is

  1769   alpha-equivalence of the term-calculi that can be specified in Ott.  This

  1742   not fixed. An example is the second part of the POPLmark challenge where

  1770   definition is rather different from ours, not using any of the nominal 

  1743   @{text "Let"}s involving patterns need to be formalised. In such situations

  1771   techniques; it also aims for maximum expressivity, covering

  1744   HOAS needs to use essentially has to represent multiple binders with

  1772   as many binding structures from programming language research as possible.

  1745   iterated single binders.

  1773   Although we were heavily inspired by their syntax, their definition of 

  1746 

  1774   alpha-equivalence was no use at all for our extension of Nominal Isabelle. 

  1747   An attempt of representing general binders in the old version of Isabelle 

  1775   First, it is far too complicated to be a basis for automated proofs 

  1748   based also on iterating single binders is described in \cite{BengtsonParow09}. 

  1776   implemented on the ML-level of Isabelle/HOL. Second, it covers cases of 

  1749   The reasoning there turned out to be quite complex. 

  1777   binders depending on other binders, which just do not make sense for 

  1750 

  1778   our alpha-equated terms, and it also allows empty types that have no meaning 

  1751   Ott is better with list dot specifications; subgrammars, is untyped; 

  1779   in a HOL-based theorem prover. For features of Ott, like subgrammars, the

  1780   datatype infrastructure in Isabelle/HOL is unfortunately not powerful 

  1781   enough. On the other hand we are not aware that Ott can make any distinction

  1782   between our three different binding modes. Also, definitions for notions like 

  1783   free-variables are work in progress in Ott.

  1784 *}

  1785 

  1786 section {* Conclusion *}

  1787 

  1788 text {*

  1789   Complication when the single scopedness restriction is lifted (two 

  1790   overlapping permutations)

  1791 

  1792   Future work: distinct list abstraction

  1793 

  1794   TODO: function definitions:

  1795   

  1796   The formalisation presented here will eventually become part of the 

  1797   Isabelle distribution, but for the moment it can be downloaded from 

  1798   the Mercurial repository linked at 

  1799   \href{http://isabelle.in.tum.de/nominal/download}

  1800   {http://isabelle.in.tum.de/nominal/download}.\medskip

  1801 

  1802   \noindent

  1803   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  

  1804   many discussions about Nominal Isabelle. We thank Peter Sewell for 

  1805   making the informal notes \cite{SewellBestiary} available to us and 

  1806   also for patiently explaining some of the finer points about the abstract 

  1807   definitions and about the implementation of the Ott-tool. We

  1808   also thank Stephanie Weirich for suggesting to separate the subgrammars

  1809   of kinds and types in our Core-Haskell example.