--- a/Nominal/NewParser.thy Fri May 21 10:47:07 2010 +0200
+++ b/Nominal/NewParser.thy Fri May 21 10:47:45 2010 +0200
@@ -11,7 +11,7 @@
ML {*
(* nominal datatype parser *)
local
- structure P = OuterParse;
+ structure P = Parse;
structure S = Scan
fun triple1 ((x, y), z) = (x, y, z)
@@ -20,9 +20,9 @@
fun tswap (((x, y), z), u) = (x, y, u, z)
in
-val _ = OuterKeyword.keyword "bind"
-val _ = OuterKeyword.keyword "bind_set"
-val _ = OuterKeyword.keyword "bind_res"
+val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "bind_set"
+val _ = Keyword.keyword "bind_res"
val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
@@ -41,7 +41,7 @@
(* binding function parser *)
val bnfun_parser =
- S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], [])
+ S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
(* main parser *)
val main_parser =
@@ -714,7 +714,7 @@
(* Command Keyword *)
-val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
+val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
(main_parser >> nominal_datatype2_cmd)
*}
--- a/Paper/Paper.thy Fri May 21 10:47:07 2010 +0200
+++ b/Paper/Paper.thy Fri May 21 10:47:45 2010 +0200
@@ -9,7 +9,7 @@
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 =)"
@@ -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 ("_ \<approx>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 \<bullet> 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 "\<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
+ 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