diff -r d73d4d151cce -r 9d8ebeded16f Paper/Paper.thy --- a/Paper/Paper.thy Fri Jul 16 02:38:19 2010 +0100 +++ b/Paper/Paper.thy Fri Jul 16 03:22:24 2010 +0100 @@ -2066,7 +2066,7 @@ representations have to resort to the iterated-single-binders-approach with all the unwanted consequences when reasoning about the resulting terms. - In a similar fashion, two formalisations involving general binders have been + Two formalisations involving general binders have been performed in older versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W \cite{BengtsonParow09, UrbanNipkow09}). Both @@ -2089,10 +2089,10 @@ 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. + is work in progress in Ott. - Although we were heavily inspired by their syntax, - their definition of $\alpha$-equivalence is unsuitable for our extension of + Although we were heavily inspired by the syntax in Ott, + its 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 @@ -2101,7 +2101,7 @@ 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 + \isacommand{bind\_res}. For example \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @@ -2114,9 +2114,9 @@ \end{center} \noindent - behave differently. In the first term-constructor, we essentially have a single - body, which happens to be ``spread'' over two arguments; in the second we have - two independent bodies, in which the same variables are bound. As a result we + in the first term-constructor we have a single + body that happens to be ``spread'' over two arguments; in the second term-constructor we have + two independent bodies in which the same variables are bound. As a result we have \begin{center} @@ -2128,58 +2128,53 @@ \end{tabular} \end{center} - Because of how we set up our definitions, we had to impose restrictions, - like a single binding function for a deep binder, that are not present in Ott. Our + \noindent + and therefore need the extra generality to be able to distinguish between + both specifications. + Because of how we set up our definitions, we also had to impose some restrictions + (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. + programming language research, for example Core-Haskell. 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 + implemented as a front-end that can be translated to OCaml with the help of a library. He presents a type-system in which the scope of general binders - can be indicated with some special markers, 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 mode \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 + can be specified using special markers, written @{text "inner"} and + @{text "outer"}. It seems our and his specifications can be + inter-translated as long as ours use the binding mode + \isacommand{bind} only. + However, we have not proved this. Pottier gives a definition for + $\alpha$-equivalence, which also uses a permutation operation (like ours). + Still, this definition is rather different from ours and he only proves that + it defines an equivalence relation. A complete reasoning infrastructure is well beyond the purposes of his language. + In a slightly different domain (programming with dependent types), the paper \cite{Altenkirch10} presents a calculus with a notion of $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}. - This definition is similar to the one by Pottier, except that it + The corresponding definition is similar to the one by Pottier, except that it has a more operational flavour and calculates a partial (renaming) map. - In this way they can handle vacuous binders. However, their notion of - equality between terms also includes rules for $\beta$ and to our - knowledge no concrete mathematical result concerning their notion + In this way Altenkirch et al can deal with vacuous binders. However, to our + best knowledge, no concrete mathematical result concerning their notion of equality has been proved. *} section {* Conclusion *} text {* - We have presented an extension of Nominal Isabelle for deriving - automatically a convenient reasoning infrastructure that can deal with - general binders, that is term-constructors binding multiple variables at - once. This extension has been tried out with the Core-Haskell - term-calculus. For such general binders, we can also extend - earlier work that derives strong induction principles which have the usual - variable convention already built in. For the moment we can do so only with manual help, - but future work will automate them completely. The code underlying the presented - extension will become part of the Isabelle distribution.\footnote{For the moment + We have presented an extension of Nominal Isabelle for dealing with + general binders, that is term-constructors having multiple bound + variables. For this extension we introduced novel definitions of + $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL. + We have tried out the extension with terms from Core-Haskell and our code + will become part of the Isabelle distribution.\footnote{For the moment it can be downloaded from the Mercurial repository linked at \href{http://isabelle.in.tum.de/nominal/download} {http://isabelle.in.tum.de/nominal/download}.} We have left out a discussion about how functions can be defined over - $\alpha$-equated terms that involve general binders. In earlier versions of Nominal + $\alpha$-equated terms involving general binders. In earlier versions of Nominal Isabelle \cite{UrbanBerghofer06} this turned out to be a thorny issue. We hope to do better this time by using the function package that has recently been implemented in Isabelle/HOL and also by restricting function @@ -2190,10 +2185,10 @@ future work. One is the exclusion of nested datatype definitions. Nested datatype definitions allow one to specify, for instance, the function kinds in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded - version @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}. For - them we need a more clever implementation than we have at the moment. + version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To + achieve this, we need a slightly more clever implementation than we have at the moment. - More interesting line of investigation is whether we can go beyond the + A 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 @@ -2204,9 +2199,7 @@ \end{center} \noindent - provide us with means to support more interesting - binding functions. - + allow us to support more interesting binding functions. We have also not yet played with other binding modes. For example we can imagine that there is need for a binding mode @@ -2214,14 +2207,14 @@ Once we feel confident about such binding modes, our implementation can be easily extended to accommodate them. - %\medskip - %\noindent - %{\bf Acknowledgements:} We are very grateful to Andrew Pitts for - %many discussions about Nominal Isabelle. We also thank Peter Sewell for - %making the informal notes \cite{SewellBestiary} available to us and - %also for patiently explaining some of the finer points of the work on the Ott-tool. - %Stephanie Weirich suggested to separate the subgrammars - %of kinds and types in our Core-Haskell example. + \medskip + \noindent + {\bf Acknowledgements:} We are very grateful to Andrew Pitts for + many discussions about Nominal Isabelle. We also thank Peter Sewell for + making the informal notes \cite{SewellBestiary} available to us and + also for patiently explaining some of the finer points of the work on the Ott-tool. + Stephanie Weirich suggested to separate the subgrammars + of kinds and types in our Core-Haskell example. *}