nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:d73d4d151cce
+:9d8ebeded16f
 example in the second part of this challenge, @{text "Let"}s involve
 patterns that bind multiple variables at once. In such situations, HOAS
 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
 use the approach based on iterated single binders. Our experience with
 the latter formalisation has been disappointing. The major pain arose from
 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.
+is work in progress in Ott.
-Although we were heavily inspired by their syntax,
+Although we were heavily inspired by the syntax in Ott,
-their definition of $\alpha$-equivalence is unsuitable for our extension of
+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
 sense for our $\alpha$-equated terms. Third, it allows empty types that have no
 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
+\isacommand{bind\_res}. For example
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
 \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t s"}\\
 \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "s"}\\
 \end{tabular}
 \end{center}
 \noindent
-behave differently. In the first term-constructor, we essentially have a single
+in the first term-constructor we have a single
-body, which happens to be ``spread'' over two arguments; in the second we have
+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
+two independent bodies in which the same variables are bound. As a result we
 have
 \begin{center}
 \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
 @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
 @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
 @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
 \end{tabular}
 \end{center}
-Because of how we set up our definitions, we had to impose restrictions,
+\noindent
-like a single binding function for a deep binder, that are not present in Ott. Our
+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
+programming language research, for example Core-Haskell.
-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.
 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
+can be specified using special markers, written @{text "inner"} and
-@{text "outer"}. With this, it seems, our and his specifications can be
+@{text "outer"}. It seems our and his specifications can be
-inter-translated, but we have not proved this. However, we believe the
+inter-translated as long as ours use the binding mode
-binding specifications in the style of Ott are a more natural way for
+\isacommand{bind} only.
-representing terms involving bindings. Pottier gives a definition for
+However, we have not proved this. Pottier gives a definition for
-$\alpha$-equivalence, which is similar to our binding mode \isacommand{bind}.
+$\alpha$-equivalence, which also uses a permutation operation (like ours).
-Although he uses also a permutation in case of abstractions, his
+Still, this definition is rather different from ours and he only proves that
-definition is rather different from ours. He proves that his notion
+it defines an equivalence relation. A complete
-of $\alpha$-equivalence is indeed a equivalence relation, but 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
+In this way Altenkirch et al can deal with vacuous binders. However, to our
-equality between terms also includes rules for $\beta$ and to our
+best knowledge, no concrete mathematical result concerning their notion
-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
+We have presented an extension of Nominal Isabelle for dealing with
-automatically a convenient reasoning infrastructure that can deal with
+general binders, that is term-constructors having multiple bound
-general binders, that is term-constructors binding multiple variables at
+variables. For this extension we introduced novel definitions of
-once. This extension has been tried out with the Core-Haskell
+$\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
-term-calculus. For such general binders, we can also extend
+We have tried out the extension with terms from Core-Haskell and our code
-earlier work that derives strong induction principles which have the usual
+will become part of the Isabelle distribution.\footnote{For the moment
-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
 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
 definitions to equivariant functions (for such functions it is possible to
 provide more automation).
 There are some restrictions we imposed in this paper, that we would like to lift in
 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
+version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
-them we need a more clever implementation than we have at the moment.
+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
 properties like
 %
 \begin{center}
 @{text "fa_ty x  =  bn x \<union> fa_bn x"}.
 \end{center}
 \noindent
-provide us with means to support more interesting
+allow us to support more interesting binding functions.
-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
 where instead of lists, we abstract lists of distinct elements.
 Once we feel confident about such binding modes, our implementation
 can be easily extended to accommodate them.
-%\medskip
+\medskip
-%\noindent
+\noindent
-%{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
+{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
-%many discussions about Nominal Isabelle. We also thank Peter Sewell for
+many discussions about Nominal Isabelle. We also thank Peter Sewell for
-%making the informal notes \cite{SewellBestiary} available to us and
+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.
+also for patiently explaining some of the finer points of the work on the Ott-tool.
-%Stephanie Weirich suggested to separate the subgrammars
+Stephanie Weirich suggested to separate the subgrammars
-%of kinds and types in our Core-Haskell example.
+of kinds and types in our Core-Haskell example.
 *}
 (*<*)
 end

changeset 2362	9d8ebeded16f
parent 2361	d73d4d151cce
child 2363	9832641ed955