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 \ 'a \ bool" abs_set2 :: "'a \ perm \ 'b \ 'c" Abs_dist :: "'a \ 'b \ 'c" - + Abs_print :: "'a \ 'b \ 'c" definition "equal \ (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 ("_ \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 \ 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 "\p q. abs_set2 (bn r\<^isub>1, t\<^isub>1) p (bn r\<^isub>2, t\<^isub>2) \ abs_set2 (bn s\<^isub>1, t\<^isub>1) q (bn s\<^isub>2, t\<^isub>2)"} - \end{center} - - \noindent - or - - \begin{center} - @{term "\p q. abs_set2 (bn r\<^isub>1 \ bn s\<^isub>1, t\<^isub>1) (p + q) (bn r\<^isub>2 \ 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