--- a/Paper/Paper.thy Thu Apr 01 18:45:50 2010 +0200
+++ b/Paper/Paper.thy Fri Apr 02 03:23:25 2010 +0200
@@ -995,8 +995,9 @@
corresponding type; the equations must be given in the binding function part of
the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s
with tuple patterns might be specified as:
-
- \begin{center}
+ %
+ \begin{equation}\label{letpat}
+ \mbox{%
\begin{tabular}{l}
\isacommand{nominal\_datatype} @{text trm} =\\
\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
@@ -1013,8 +1014,8 @@
\isacommand{where}~@{text "bn(PNil) = []"}\\
\hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
\hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
In this specification the function @{text "bn"} determines which atoms of @{text p} are
@@ -1082,8 +1083,8 @@
\hspace{5mm}\phantom{$\mid$}\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
\;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
- \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
- \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},
+ \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}\\
+ \hspace{20mm}\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\
\isacommand{and} {\it assn} =\\
\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
@@ -1293,12 +1294,14 @@
context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
This is a phenomenon
that has also been pointed out in \cite{ott-jfp}. We can also see that
- given a @{text "bn"}-function for a type @{text "ty"}, we have that
%
\begin{equation}\label{bnprop}
@{text "fv_ty x = bn x \<union> fv_bn x"}.
\end{equation}
+ \noindent
+ holds for any @{text "bn"}-function of type @{text "ty"}.
+
Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions,
we also need to define auxiliary alpha-equivalence relations for the binding functions.
@@ -1630,41 +1633,80 @@
as well. To avoid this we introduce a new construction operation
that applies a permutation under a binding function.
- For each binding function @{text "bn\<^isub>j :: ty\<^isub>i \<Rightarrow> \<dots>"} we define a permutation operation
- @{text "\<bullet>bn\<^isub>j\<^isub> :: perm \<Rightarrow> ty\<^isub>i \<Rightarrow> ty\<^isub>i"}. This operation permutes only the arguments
- that are bound by the binding function while also descending in the recursive subcalls.
- For each term constructor @{text "C x\<^isub>1 \<dots> x\<^isub>n"} the @{text "\<bullet>bn\<^isub>j"} operation applied
- to a permutation @{text "\<pi>"} and to this constructor equals the constructor applied
- to the values for each argument. Provided @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, the value
- for an argument @{text "x\<^isub>j"} is:
- \begin{center}
- \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
- $\bullet$ & @{text "x\<^isub>i"} provided @{text "x\<^isub>i"} is not in @{text "rhs"}\\
- $\bullet$ & @{text "\<pi> \<bullet> x\<^isub>i"} provided @{text "x\<^isub>i"} is in @{text "rhs"} without a binding function\\
- $\bullet$ & @{text "\<pi> \<bullet>bn\<^isub>k x\<^isub>i"} provided @{text "bn\<^isub>k x\<^isub>i"} is @{text "rhs"}\\
- \end{tabular}
- \end{center}
-
- The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it
- and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this definition is correct is:
-
-%% We could get this from ExLet/perm_bn lemma.
- \begin{lemma} For every bn function @{text "bn\<^isup>\<alpha>\<^isub>i"},
- \begin{eqnarray}
- @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\
- @{text "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}
- \end{eqnarray}
- \end{lemma}
- \begin{proof} By induction on the lifted type it follows from the definitions of
- permutations on the lifted type and the lifted defining equations of @{text "\<bullet>bn"}
- and @{text "fv_bn"}.
- \end{proof}
-
*}
section {* Strong Induction Principles *}
text {*
+ In the previous section we were able to provide induction principles that
+ allow us to perform structural inductions over alpha-equated terms.
+ We call such induction principles \emph{weak}, because in case of a term-contructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
+ the induction hypothesis requires us to establish the implication
+ %
+ \begin{equation}\label{weakprem}
+ @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
+ \end{equation}
+
+ \noindent
+ where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
+ The problem with this implication is that in general it is not easy to establish.
+ The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"}
+ (for example we cannot assume the variable convention).
+
+ In \cite{UrbanTasson05} we introduced a method for automatically
+ strengthening weak induction principles for terms containing single
+ binders. These stronger induction principles allow us to make additional
+ assumptions about binders. These additional assumptions amount to a formal
+ version of the usual variable convention for binders. A natural question is
+ whether we can also strengthen the weak induction principles in the presence
+ general binders. We will indeed be able to so, but for this we need an
+ additional notion of permuting deep binders.
+
+ Given a binding function @{text "bn"} we need to define an auxiliary permutation
+ operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
+ Given a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
+ %
+ \begin{center}
+ @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}
+ \end{center}
+
+ \noindent
+ with @{text "y\<^isub>i"} determined as follows:
+ %
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
+ $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\
+ $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\
+ $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Using the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to alpha
+ equated terms. We can then prove
+
+ \begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"}. Then
+ {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}
+ for all permutations @{text p}, @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
+ \end{lemma}
+
+ \begin{proof}
+ By induction on @{text x}. The equation follow by simple unfolding
+ of the definitions.
+ \end{proof}
+
+ This allows is to strengthen the induction principles. We will explain
+ the details with the @{text "Let"} term-constructor from \eqref{letpat}.
+ Instead of establishing the implication
+
+ \begin{center}
+ a
+ \end{center}
+
+ \noindent
+ from the weak induction principle.
+
+
With the help of @{text "\<bullet>bn"} functions defined in the previous section
we can show that binders can be substituted in term constructors. We show
this only for the specification from Figure~\ref{nominalcorehas}. The only
@@ -1720,6 +1762,8 @@
}
\end{equation}
+
+
*}
text {*
@@ -1799,115 +1843,109 @@
section {* Related Work *}
text {*
- To our knowledge the earliest usage of general binders in a theorem prover
+ To our knowledge, the earliest usage of general binders in a theorem prover
is described in \cite{NaraschewskiNipkow99} about a formalisation of the
algorithm W. This formalisation implements binding in type schemes using a
- de-Bruijn indices representation. Since type schemes contain only a single
+ de-Bruijn indices representation. Since type schemes of W contain only a single
binder, different indices do not refer to different binders (as in the usual
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
+ 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
- kinds of de-Bruijn indices comes for free in any modern theorem prover 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, requires additional predicates that filter out some unwanted
- terms. Our guess is that they results in rather intricate formal reasoning.
- Also one motivation of our work is that the user does not need to know
- anything at all about de-Bruijn indices, which are of course visible in the
- usual de-Bruijn indices representations, but also in locally nameless
- representations.
+ representations of bindings comes for free in the theorem provers Isabelle/HOL and
+ Coq, for example, 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
+ intricate formal reasoning.
Another representation technique for binding is higher-order abstract syntax
- (HOAS), for example implemented in the Twelf system. This representation
+ (HOAS), which for example is implemented in the Twelf system. This representation
technique supports very elegantly many aspects of \emph{single} binding, and
impressive work is in progress that uses HOAS for mechanising the metatheory
- of SML \cite{LeeCraryHarper07}. We are, however, not aware how multiple binders of SML
- are represented in this work. Judging from the submitted Twelf-solution for the
- POPLmark challenge, HOAS cannot easily deal with binding
- constructs where the number of bound variables is not fixed. For 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, essentially, to the iterated-single-binders-approach with all the unwanted
- consequences for reasoning about terms.
+ of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple
+ binders of SML are represented in this work. Judging from the submitted
+ Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with
+ binding constructs where the number of bound variables is not fixed. For
+ 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.
- Two formalisations involving general binders have been performed in older
+ Two formalisations involving general binders have also been performed in older
versions of Nominal Isabelle \cite{BengtsonParow09, UrbanNipkow09}. Both
- use also the approach based on iterated single binders. Our experience with the
- latter formalisation has been disappointing. The major pain arises
- from the need to ``unbind'' variables. This can be done in one step with our
+ 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
- iteration with single binders. The resulting formal reasoning is rather
- unpleasant. The hope is that the extension presented in this paper is a
- substantial improvement.
+ 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 is the description of the Ott-tool
- \cite{ott-jfp}. This tool is a nifty front-end for creating \LaTeX{}
- documents from term-calculi specifications. For a subset of the
- specifications, Ott can also generate theorem prover code using a raw
- representation and in Coq also a locally nameless representation for
- terms. The developers of this tool have also put forward (on paper) a
- definition for the notion of alpha-equivalence of the term-calculi that can
- be specified in Ott. This definition is rather different from ours, not
- using any nominal techniques; it also aims for maximum expressivity,
- covering as many binding structures from programming language research as
- possible. Although we were heavily inspired by their syntax, their
- definition of alpha-equivalence was no use at all for our extension of
+ 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,
+ 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. It also allows empty types that have
- no meaning in a HOL-based theorem prover.
+ sense for our alpha-equated terms. Third, it allows empty types that have no
+ meaning in a HOL-based theorem prover.
- Because of how we set up our definitions, we had to impose some
- restrictions, like excluding overlapping deep binders, which are not present
- in Ott. Our expectation is that we can still cover many interesting term-calculi
- from programming language research, like Core-Haskell. For features of Ott,
- like subgrammars, the datatype infrastructure in Isabelle/HOL is
- unfortunately not yet powerful enough to implement them. On the other hand
- we are not aware that Ott can make any distinction between our three
- different binding modes. Also, definitions for notions like free-variables
- are work in progress in Ott. Since Ott produces either raw representations
- or locally nameless representations it can largely rely on the reasoning
- infrastructure derived automatically by the theorem provers. In contrast,
- have to make considerable effort to establish a reasoning infrastructure
- for alpha-equated terms.
+ 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
+ expectation is that we can still cover many interesting term-calculi from
+ programming language research, for example Core-Haskell. For prviding 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.
*}
section {* Conclusion *}
text {*
- We have presented an extension for Nominal Isabelle in order to derive a
- convenient reasoning infrastructure for term-constructors binding multiple
- variables at once. This extension can deal with term-calculi such as
- Core-Haskell. For such calculi, we can also derive strong induction
- principles that have the usual variable already built in. At the moment we
- can do so only with manual help, but future work will automate them
- completely. The code underlying this extension will become part of the
- Isabelle distribution, but for the moment it can be downloaded from the
- Mercurial repository linked at
+ 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. At 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, but 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 with general binders. In earlier work \cite{UrbanBerghofer06}
- this turned out to be a thorny issue for Nominal Isabelle.
- 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).
+ 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
+ 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, like the absence of nested type
- definitions that allow one to specify the function kinds as
- @{text "TFun string (ty list)"} instead of the unfolded version
- @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}; such
- restrictions can be easily lifted. They essentially amount to 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
+ There are some restrictions we imposed in this paper, we 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
+ 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}
@@ -1918,8 +1956,9 @@
\end{center}
\noindent
- where the deep binders @{text "bn(r)"} and @{text "bn(s)"} overlap..
- We would need to implement such bindings with alpha-equivalences like
+ 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)"}
@@ -1934,16 +1973,24 @@
\noindent
Both versions require two permutations (for each binding). But unfortunately the
- first version cannot not work since it leaves unbound atoms that should be
+ 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 \cite{SewellBestiary}.
- This clearly needs more investigation.
+ 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 of binding function 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.
+
We have also not yet played with other binding modes. For example we can
- imagine that the here is a mode \isacommand{bind\_\#list} with the associated
- alpha-equivalence definition
+ imagine that there is need for a binding mode \isacommand{bind\_\#list} with an associated
+ alpha-equivalence definition as follows:
%
\begin{center}
$\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
@@ -1957,18 +2004,16 @@
\end{center}
\noindent
- In this definition we added the requirement that all bound variables
- in a list are distinct. We can imagine applications for such a notion
- of binding, but have not explored them yet. Our implementation can
- easily extended to accommodate further binding modes.
+ In this definition we added the requirement that all bound variables in a
+ list are distinct. 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 thank Peter Sewell for
making the informal notes \cite{SewellBestiary} available to us and
- also for patiently explaining some of the finer points about the abstract
- definitions and about the implementation of the Ott-tool. We
+ also for patiently explaining some of the finer points of the work on the Ott-tool. We
also thank Stephanie Weirich for suggesting to separate the subgrammars
of kinds and types in our Core-Haskell example.
*}