nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:029f8aabed12
+:5dc48e1af733
 fv :: "'a \<Rightarrow> 'b"
 abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 alpha_bn :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 abs_set2 :: "'a \<Rightarrow> perm \<Rightarrow> 'b \<Rightarrow> 'c"
 Abs_dist :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
+Abs_print :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
 definition
 "equal \<equiv> (op =)"
 notation (latex output)
 alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
 Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
 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 ("_ \<approx>bn _")
 (*>*)
 \begin{center}
 @{text "t ::= x | t t | \<lambda>x. t"}
 \end{center}
 \noindent
-where free and bound variables have names.  For such alpha-equated terms,  Nominal Isabelle
+where free and bound variables have names.  For such alpha-equated terms,
-derives automatically a reasoning infrastructure that has been used
+Nominal Isabelle derives automatically a reasoning infrastructure that has
-successfully in formalisations of an equivalence checking algorithm for LF
+been used successfully in formalisations of an equivalence checking
-\cite{UrbanCheneyBerghofer08}, Typed
+algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed
 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-\cite{BengtsonParow09} and a strong normalisation result
+\cite{BengtsonParow09} and a strong normalisation result for cut-elimination
-for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been
+in classical logic \cite{UrbanZhu08}. It has also been used by Pollack for
-used by Pollack for formalisations in the locally-nameless approach to
+formalisations in the locally-nameless approach to binding
-binding \cite{SatoPollack10}.
+\cite{SatoPollack10}.
 However, Nominal Isabelle has fared less well in a formalisation of
 the algorithm W \cite{UrbanNipkow09}, where types and type-schemes are,
 respectively, of the form
 %
 @{term "\<forall>p. p \<bullet> f = f"}
 \end{equation}
 \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 \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
 @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
 Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
 \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]}
 \end{equation}
 \noindent
 The first mode is for binding lists of atoms (the order of binders matters);
 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}.
+``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
+Ott, we allow multiple labels in binders and bodies. For example we allow
-In contrast to Ott, we allow multiple labels in binders and bodies. For example
+binding clauses of the form:
-we allow binding clauses of the form:
 \begin{center}
 \begin{tabular}{@ {}ll@ {}}
 @{text "Foo\<^isub>1 x::name y::name t::lam s::lam"} &
 \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
 \end{tabular}
 \end{center}
 \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
+and \isacommand{bind\_res} the binding clauses will make a difference to the semantics
-terms of the corresponding alpha-equivalence. We will show this later with an example.
+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
 distinguish between \emph{shallow} and \emph{deep} binders.  Shallow binders
 are just labels. The restriction we need to impose on them is that in case
 \end{center}
 \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
+\isacommand{bind\_set} or \isacommand{bind} in the second case makes again a
-difference to the underlying notion of alpha-equivalence. Note also that in
+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.
 A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
 \noindent
 where the argument of the deep binder is also in the body. We call such
 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@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}\\
 \hspace{5mm}\phantom{$\mid$}\ldots\\
 \noindent
 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
+function and alpha-equivalence relation, which we are going to define below.
-rest of this section.
+For this definition, we have to impose some restrictions on deep binders. First,
-The restriction we have to impose on deep binders is that we cannot have
+we cannot have more than one binding function for one binder. So we exclude:
-more than one binding function for one binder. So we exclude:
 \begin{center}
 \begin{tabular}{ll}
 @{text "Baz p::pat t::trm"} &
 \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
 later on.
 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
+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 "label"}. In case
+clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
 of the lambda-calculus, the completion produces
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} =\\
 \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>1 t\<^isub>2"}\\
-\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>2"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}
 \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\
 \end{tabular}
 \end{center}
 de-Bruijn representation), but to different bound variables. A similar idea
 has been recently explored for general binders in the locally nameless
 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
 (HOAS), which for example is implemented in the Twelf system. This representation
 technique supports very elegantly many aspects of \emph{single} binding, and
 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.
 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
+The most closely related work to the one presented here is the Ott-tool
-nifty front-end for creating \LaTeX{} documents from specifications of
+\cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
-term-calculi involving general binders. For a subset of the specifications, Ott can also generate
+front-end for creating \LaTeX{} documents from specifications of
-theorem prover code using a raw representation of terms, and in Coq also a
+term-calculi involving general binders. For a subset of the specifications,
-locally nameless representation. The developers of this tool have also put
+Ott can also generate theorem prover code using a raw representation of
-forward (on paper) a definition for alpha-equivalence of terms that can be
+terms, and in Coq also a locally nameless representation. The developers of
-specified in Ott.  This definition is rather different from ours, not using
+this tool have also put forward (on paper) a definition for
-any nominal techniques. Although we were heavily inspired by their syntax,
+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
+three different binding modes.
-variables of a term are work in progress in Ott.
+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 *}
 text {*
 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.
-More
+More interesting line of investigation is whether we can go beyond the
-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 "\<exists>p q. abs_set2 (bn r\<^isub>1, t\<^isub>1) p (bn r\<^isub>2, t\<^isub>2) \<and> abs_set2 (bn s\<^isub>1, t\<^isub>1) q (bn s\<^isub>2, t\<^isub>2)"}
-\end{center}
-\noindent
-or
-\begin{center}
-@{term "\<exists>p q. abs_set2 (bn r\<^isub>1 \<union> bn s\<^isub>1, t\<^isub>1) (p + q)  (bn r\<^isub>2 \<union> 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
 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 \eqref{bnprop} provide us with means to support more interesting
 binding functions.

changeset 2163	5dc48e1af733
parent 2156	029f8aabed12
child 2175	f11dd09fa3a7