# HG changeset patch # User Christian Urban # Date 1270093212 -7200 # Node ID 2afee29cf81cb4eab37cbb4010827d8938bc7c2e # Parent 468c3c1adcba6bc7f795d6f92c9fca70d095d542 completed related work section diff -r 468c3c1adcba -r 2afee29cf81c Paper/Paper.thy --- 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