--- a/LMCS-Paper/Paper.thy Mon Aug 15 17:42:35 2011 +0200
+++ b/LMCS-Paper/Paper.thy Tue Aug 16 17:48:09 2011 +0200
@@ -59,11 +59,15 @@
section {* Introduction *}
text {*
+ So far, Nominal Isabelle provided a mechanism for constructing alpha-equated
+ terms, for example lambda-terms
- So far, Nominal Isabelle provided a mechanism for constructing
- $\alpha$-equated terms, for example lambda-terms,
- @{text "t ::= x | t t | \<lambda>x. t"},
- where free and bound variables have names. For such $\alpha$-equated terms,
+ \[
+ @{text "t ::= x | t t | \<lambda>x. t"}
+ \]\smallskip
+
+ \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
@@ -73,75 +77,71 @@
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,
+ 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
- %
+
\begin{equation}\label{tysch}
\begin{array}{l}
- @{text "T ::= x | T \<rightarrow> T"}\hspace{9mm}
+ @{text "T ::= x | T \<rightarrow> T"}\hspace{15mm}
@{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
\end{array}
- \end{equation}
- %
+ \end{equation}\smallskip
+
\noindent
and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
type-variables. While it is possible to implement this kind of more general
binders by iterating single binders, this leads to a rather clumsy
- formalisation of W.
- The need of iterating single binders is also one reason
- why Nominal Isabelle
- and similar theorem provers that only provide
- mechanisms for binding single variables
- has not fared extremely well with the
- more advanced tasks in the POPLmark challenge \cite{challenge05}, because
- also there one would like to bind multiple variables at once.
+ formalisation of W. The need of iterating single binders is also one reason
+ why Nominal Isabelle and similar theorem provers that only provide
+ mechanisms for binding single variables has not fared extremely well with
+ the more advanced tasks in the POPLmark challenge \cite{challenge05},
+ because also there one would like to bind multiple variables at once.
Binding multiple variables has interesting properties that cannot be captured
easily by iterating single binders. For example in the case of type-schemes we do not
want to make a distinction about the order of the bound variables. Therefore
- we would like to regard the first pair of type-schemes as $\alpha$-equivalent,
+ we would like to regard the first pair of type-schemes as alpha-equivalent,
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
- the second pair should \emph{not} be $\alpha$-equivalent:
- %
+ the second pair should \emph{not} be alpha-equivalent:
+
\begin{equation}\label{ex1}
@{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"}\hspace{10mm}
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
- \end{equation}
- %
+ \end{equation}\smallskip
+
\noindent
- Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ
+ Moreover, we like to regard type-schemes as alpha-equivalent, if they differ
only on \emph{vacuous} binders, such as
- %
+
\begin{equation}\label{ex3}
@{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, z}. x \<rightarrow> y"}
- \end{equation}
- %
+ \end{equation}\smallskip
+
\noindent
where @{text z} does not occur freely in the type. In this paper we will
- give a general binding mechanism and associated notion of $\alpha$-equivalence
+ give a general binding mechanism and associated notion of alpha-equivalence
that can be used to faithfully represent this kind of binding in Nominal
- Isabelle.
- The difficulty of finding the right notion for $\alpha$-equivalence
+ Isabelle. The difficulty of finding the right notion for alpha-equivalence
can be appreciated in this case by considering that the definition given by
- Leroy in \cite{Leroy92} is incorrect (it omits a side-condition).
+ Leroy in \cite[Page ???]{Leroy92} is incorrect (it omits a side-condition).
- However, the notion of $\alpha$-equivalence that is preserved by vacuous
+ However, the notion of alpha-equivalence that is preserved by vacuous
binders is not always wanted. For example in terms like
- %
+
\begin{equation}\label{one}
@{text "\<LET> x = 3 \<AND> y = 2 \<IN> x - y \<END>"}
- \end{equation}
+ \end{equation}\smallskip
\noindent
we might not care in which order the assignments @{text "x = 3"} and
- \mbox{@{text "y = 2"}} are given, but it would be often unusual to regard
- \eqref{one} as $\alpha$-equivalent with
- %
- \begin{center}
+ \mbox{@{text "y = 2"}} are given, but it would be often unusual (particularly
+ in strict languages) to regard \eqref{one} as alpha-equivalent with
+
+ \[
@{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = foo \<IN> x - y \<END>"}
- \end{center}
- %
+ \]\smallskip
+
\noindent
Therefore we will also provide a separate binding mechanism for cases in
which the order of binders does not matter, but the ``cardinality'' of the
@@ -150,134 +150,129 @@
However, we found that this is still not sufficient for dealing with
language constructs frequently occurring in programming language
research. For example in @{text "\<LET>"}s containing patterns like
- %
+
\begin{equation}\label{two}
@{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
- \end{equation}
- %
+ \end{equation}\smallskip
+
\noindent
we want to bind all variables from the pattern inside the body of the
$\mathtt{let}$, but we also care about the order of these variables, since
- we do not want to regard \eqref{two} as $\alpha$-equivalent with
- %
- \begin{center}
+ we do not want to regard \eqref{two} as alpha-equivalent with
+
+ \[
@{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
- \end{center}
- %
+ \]\smallskip
+
\noindent
As a result, we provide three general binding mechanisms each of which binds
multiple variables at once, and let the user chose which one is intended
- in a formalisation.
- %%when formalising a term-calculus.
+ when formalising a term-calculus.
By providing these general binding mechanisms, however, we have to work
around a problem that has been pointed out by Pottier \cite{Pottier06} and
Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form
- %
- \begin{center}
+
+ \[
@{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
- \end{center}
- %
+ \]\smallskip
+
\noindent
- we care about the
- information that there are as many bound variables @{text
+ we care about the information that there are as many bound variables @{text
"x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if
we represent the @{text "\<LET>"}-constructor by something like
- %
- \begin{center}
+
+ \[
@{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s) [t\<^isub>1,\<dots>,t\<^isub>n]"}
- \end{center}
- %
+ \]\smallskip
+
\noindent
where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text
"x\<^isub>i"} becomes bound in @{text s}. In this representation the term
- \mbox{@{text "\<LET> (\<lambda>x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
- instance, but the lengths of the two lists do not agree. To exclude such
- terms, additional predicates about well-formed terms are needed in order to
- ensure that the two lists are of equal length. This can result in very messy
- reasoning (see for example~\cite{BengtsonParow09}). To avoid this, we will
- allow type specifications for @{text "\<LET>"}s as follows
- %
- \begin{center}
- \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
- @{text trm} & @{text "::="} & @{text "\<dots>"}
- & @{text "|"} @{text "\<LET> as::assn s::trm"}\hspace{2mm}
- \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\%%%[1mm]
- @{text assn} & @{text "::="} & @{text "\<ANIL>"}
- & @{text "|"} @{text "\<ACONS> name trm assn"}
- \end{tabular}
- \end{center}
- %
+ \mbox{@{text "\<LET> (\<lambda>x . s) [t\<^isub>1, t\<^isub>2]"}} is a perfectly
+ legal instance, but the lengths of the two lists do not agree. To exclude
+ such terms, additional predicates about well-formed terms are needed in
+ order to ensure that the two lists are of equal length. This can result in
+ very messy reasoning (see for example~\cite{BengtsonParow09}). To avoid
+ this, we will allow type specifications for @{text "\<LET>"}s as follows
+
+ \[
+ \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll}
+ @{text trm} & @{text "::="} & @{text "\<dots>"} \\
+ & @{text "|"} & @{text "\<LET> as::assn s::trm"}\hspace{2mm}
+ \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
+ @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
+ & @{text "|"} & @{text "\<ACONS> name trm assn"}
+ \end{tabular}}
+ \]\smallskip
+
\noindent
where @{text assn} is an auxiliary type representing a list of assignments
and @{text bn} an auxiliary function identifying the variables to be bound
by the @{text "\<LET>"}. This function can be defined by recursion over @{text
assn} as follows
- %
- \begin{center}
- @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm}
+
+ \[
+ @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{10mm}
@{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"}
- \end{center}
- %
+ \]\smallskip
+
\noindent
The scope of the binding is indicated by labels given to the types, for
example @{text "s::trm"}, and a binding clause, in this case
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
- clause states that all the names the function @{text
- "bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily
- inspired by the syntax of the Ott-tool \cite{ott-jfp}.
-
- Though, Ott
- has only one binding mode, namely the one where the order of
- binders matters. Consequently, type-schemes with binding sets
- of names cannot be modelled in Ott.
+ clause states that all the names the function @{text "bn(as)"} returns
+ should be bound in @{text s}. This style of specifying terms and bindings
+ is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work
+ extends Ott in several aspects: one is that we support three binding
+ modes---Ott has only one, namely the one where the order of binders matters.
+ Another is that our reasoning infrastructure, like the notion of support and
+ strong induction principles, is derived from first principles within the
+ Isabelle/HOL theorem prover.
However, we will not be able to cope with all specifications that are
- allowed by Ott. One reason is that Ott lets the user specify ``empty''
- types like @{text "t ::= t t | \<lambda>x. t"}
- where no clause for variables is given. Arguably, such specifications make
- some sense in the context of Coq's type theory (which Ott supports), but not
- at all in a HOL-based environment where every datatype must have a non-empty
- set-theoretic model. % \cite{Berghofer99}.
+ allowed by Ott. One reason is that Ott lets the user specify ``empty'' types
+ like \mbox{@{text "t ::= t t | \<lambda>x. t"}} where no clause for variables is
+ given. Arguably, such specifications make some sense in the context of Coq's
+ type theory (which Ott supports), but not at all in a HOL-based environment
+ where every datatype must have a non-empty set-theoretic model
+ \cite{Berghofer99}. Another reason is that we establish the reasoning
+ infrastructure for alpha-\emph{equated} terms. In contrast, Ott produces a
+ reasoning infrastructure in Isabelle/HOL for \emph{non}-alpha-equated, or
+ ``raw'', terms. While our alpha-equated terms and the raw terms produced by
+ Ott use names for bound variables, there is a key difference: working with
+ alpha-equated terms means, for example, that the two type-schemes
- Another reason is that we establish the reasoning infrastructure
- for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning
- infrastructure in Isabelle/HOL for
- \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms
- and the raw terms produced by Ott use names for bound variables,
- there is a key difference: working with $\alpha$-equated terms means, for example,
- that the two type-schemes
-
- \begin{center}
+ \[
@{text "\<forall>{x}. x \<rightarrow> y = \<forall>{x, z}. x \<rightarrow> y"}
- \end{center}
+ \]\smallskip
\noindent
- are not just $\alpha$-equal, but actually \emph{equal}! As a result, we can
- only support specifications that make sense on the level of $\alpha$-equated
+ are not just alpha-equal, but actually \emph{equal}! As a result, we can
+ only support specifications that make sense on the level of alpha-equated
terms (offending specifications, which for example bind a variable according
to a variable bound somewhere else, are not excluded by Ott, but we have
to).
- Our insistence on reasoning with $\alpha$-equated terms comes from the
+ Our insistence on reasoning with alpha-equated terms comes from the
wealth of experience we gained with the older version of Nominal Isabelle:
- for non-trivial properties, reasoning with $\alpha$-equated terms is much
+ for non-trivial properties, reasoning with alpha-equated terms is much
easier than reasoning with raw terms. The fundamental reason for this is
that the HOL-logic underlying Nominal Isabelle allows us to replace
``equals-by-equals''. In contrast, replacing
- ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms
+ ``alpha-equals-by-alpha-equals'' in a representation based on raw terms
requires a lot of extra reasoning work.
- Although in informal settings a reasoning infrastructure for $\alpha$-equated
+ Although in informal settings a reasoning infrastructure for alpha-equated
terms is nearly always taken for granted, establishing it automatically in
Isabelle/HOL is a rather non-trivial task. For every
specification we will need to construct type(s) containing as elements the
- $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
+ alpha-equated terms. To do so, we use the standard HOL-technique of defining
a new type by identifying a non-empty subset of an existing type. The
construction we perform in Isabelle/HOL can be illustrated by the following picture:
- %
- \begin{center}
- \begin{tikzpicture}[scale=0.89]
+
+ \[
+ \mbox{\begin{tikzpicture}[scale=1.1]
%\draw[step=2mm] (-4,-1) grid (4,1);
\draw[very thick] (0.7,0.4) circle (4.25mm);
@@ -290,28 +285,28 @@
\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
\draw (1.8, 0.48) node[right=-0.1mm]
- {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+ {\small\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
- \draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+ \draw (-3.25, 0.55) node {\small\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};
- \end{tikzpicture}
- \end{center}
- %
+ \end{tikzpicture}}
+ \]\smallskip
+
\noindent
We take as the starting point a definition of raw terms (defined as a
- datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in
- the type of sets of raw terms according to our $\alpha$-equivalence relation,
- and finally define the new type as these $\alpha$-equivalence classes
- (non-emptiness is satisfied whenever the raw terms are definable as datatype
- in Isabelle/HOL and our relation for $\alpha$-equivalence is
- an equivalence relation).
+ datatype in Isabelle/HOL); then identify the alpha-equivalence classes in
+ the type of sets of raw terms according to our alpha-equivalence relation,
+ and finally define the new type as these alpha-equivalence classes (the
+ non-emptiness requirement is always satisfied whenever the raw terms are
+ definable as datatype in Isabelle/HOL and our relation for alpha-equivalence
+ is an equivalence relation).
The fact that we obtain an isomorphism between the new type and the
non-empty subset shows that the new type is a faithful representation of
- $\alpha$-equated terms. That is not the case for example for terms using the
+ alpha-equated terms. That is not the case for example for terms using the
locally nameless representation of binders \cite{McKinnaPollack99}: in this
representation there are ``junk'' terms that need to be excluded by
reasoning about a well-formedness predicate.
@@ -322,18 +317,18 @@
task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package
described by Homeier \cite{Homeier05} for the HOL4 system. This package
allows us to lift definitions and theorems involving raw terms to
- definitions and theorems involving $\alpha$-equated terms. For example if we
+ definitions and theorems involving alpha-equated terms. For example if we
define the free-variable function over raw lambda-terms
\begin{center}
- @{text "fv(x) = {x}"}\hspace{8mm}
- @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}
- @{text "fv(\<lambda>x.t) = fv(t) - {x}"}
+ @{text "fv(x) \<equiv> {x}"}\\
+ @{text "fv(t\<^isub>1 t\<^isub>2) \<equiv> fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}
+ @{text "fv(\<lambda>x.t) \<equiv> fv(t) - {x}"}
\end{center}
\noindent
then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
- operating on quotients, or $\alpha$-equivalence classes of lambda-terms. This
+ operating on quotients, or alpha-equivalence classes of lambda-terms. This
lifted function is characterised by the equations
\begin{center}
@@ -345,16 +340,16 @@
\noindent
(Note that this means also the term-constructors for variables, applications
and lambda are lifted to the quotient level.) This construction, of course,
- only works if $\alpha$-equivalence is indeed an equivalence relation, and the
- ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence.
+ only works if alpha-equivalence is indeed an equivalence relation, and the
+ ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence.
For example, we will not be able to lift a bound-variable function. Although
this function can be defined for raw terms, it does not respect
- $\alpha$-equivalence and therefore cannot be lifted.
+ alpha-equivalence and therefore cannot be lifted.
To sum up, every lifting
of theorems to the quotient level needs proofs of some respectfulness
properties (see \cite{Homeier05}). In the paper we show that we are able to
automate these proofs and as a result can automatically establish a reasoning
- infrastructure for $\alpha$-equated terms.\smallskip
+ infrastructure for alpha-equated terms.\smallskip
The examples we have in mind where our reasoning infrastructure will be
helpful includes the term language of Core-Haskell. This term language
@@ -366,17 +361,17 @@
\noindent
{\bf Contributions:} We provide three new definitions for when terms
- involving general binders are $\alpha$-equivalent. These definitions are
+ involving general binders are alpha-equivalent. These definitions are
inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
- proofs, we establish a reasoning infrastructure for $\alpha$-equated
+ proofs, we establish a reasoning infrastructure for alpha-equated
terms, including properties about support, freshness and equality
- conditions for $\alpha$-equated terms. We are also able to derive strong
+ conditions for alpha-equated terms. We are also able to derive strong
induction principles that have the variable convention already built in.
The method behind our specification of general binders is taken
from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
- that our specifications make sense for reasoning about $\alpha$-equated terms.
+ that our specifications make sense for reasoning about alpha-equated terms.
The main improvement over Ott is that we introduce three binding modes
- (only one is present in Ott), provide formalised definitions for $\alpha$-equivalence and
+ (only one is present in Ott), provide formalised definitions for alpha-equivalence and
for free variables of our terms, and also derive a reasoning infrastructure
for our specifications from ``first principles''.
@@ -499,7 +494,7 @@
The most original aspect of the nominal logic work of Pitts is a general
definition for the notion of the ``set of free variables of an object @{text
"x"}''. This notion, written @{term "supp x"}, is general in the sense that
- it applies not only to lambda-terms ($\alpha$-equated or not), but also to lists,
+ it applies not only to lambda-terms (alpha-equated or not), but also to lists,
products, sets and even functions. The definition depends only on the
permutation operation and on the notion of equality defined for the type of
@{text x}, namely:
@@ -520,9 +515,9 @@
@{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
- \begin{myproperty}\label{swapfreshfresh}
+ \begin{prop}\label{swapfreshfresh}
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
- \end{myproperty}
+ \end{prop}
While often the support of an object can be relatively easily
described, for example for atoms, products, lists, function applications,
@@ -553,20 +548,20 @@
such approximations can be simplified with the notion \emph{supports}, defined
as follows:
- \begin{definition}
+ \begin{defi}
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
- \end{definition}
+ \end{defi}
\noindent
The main point of @{text supports} is that we can establish the following
two properties.
- \begin{myproperty}\label{supportsprop}
+ \begin{prop}\label{supportsprop}
Given a set @{text "as"} of atoms.
{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
{\it (ii)} @{thm supp_supports[no_vars]}.
- \end{myproperty}
+ \end{prop}
Another important notion in the nominal logic work is \emph{equivariance}.
For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant
@@ -605,16 +600,16 @@
proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
- \begin{myproperty}\label{supppermeq}
+ \begin{prop}\label{supppermeq}
@{thm[mode=IfThen] supp_perm_eq[no_vars]}
- \end{myproperty}
+ \end{prop}
- \begin{myproperty}\label{avoiding}
+ \begin{prop}\label{avoiding}
For a finite set @{text as} and a finitely supported @{text x} with
@{term "as \<sharp>* x"} and also a finitely supported @{text c}, there
exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and
@{term "supp x \<sharp>* p"}.
- \end{myproperty}
+ \end{prop}
\noindent
The idea behind the second property is that given a finite set @{text as}
@@ -628,7 +623,7 @@
Most properties given in this section are described in detail in \cite{HuffmanUrban10}
and all are formalised in Isabelle/HOL. In the next sections we will make
- extensive use of these properties in order to define $\alpha$-equivalence in
+ extensive use of these properties in order to define alpha-equivalence in
the presence of multiple binders.
*}
@@ -651,8 +646,8 @@
"as"} in the body @{text "x"}.
The first question we have to answer is when two pairs @{text "(as, x)"} and
- @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in
- the notion of $\alpha$-equivalence that is \emph{not} preserved by adding
+ @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in
+ the notion of alpha-equivalence that is \emph{not} preserved by adding
vacuous binders.) To answer this question, we identify four conditions: {\it (i)}
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
@@ -675,16 +670,16 @@
%
\noindent
Note that this relation depends on the permutation @{text
- "p"}; $\alpha$-equivalence between two pairs is then the relation where we
+ "p"}; alpha-equivalence between two pairs is then the relation where we
existentially quantify over this @{text "p"}. Also note that the relation is
dependent on a free-atom function @{text "fa"} and a relation @{text
"R"}. The reason for this extra generality is that we will use
- $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In
+ $\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
the latter case, @{text R} will be replaced by equality @{text "="} and we
will prove that @{text "fa"} is equal to @{text "supp"}.
The definition in \eqref{alphaset} does not make any distinction between the
- order of abstracted atoms. If we want this, then we can define $\alpha$-equivalence
+ order of abstracted atoms. If we want this, then we can define alpha-equivalence
for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
as follows
%
@@ -717,7 +712,7 @@
\end{equation}
It might be useful to consider first some examples how these definitions
- of $\alpha$-equivalence pan out in practice. For this consider the case of
+ of alpha-equivalence pan out in practice. For this consider the case of
abstracting a set of atoms over types (as in type-schemes). We set
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we
define
@@ -729,7 +724,7 @@
\noindent
Now recall the examples shown in \eqref{ex1} and
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
- @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
+ @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{set+}}$ by taking @{text p} to
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
@@ -741,7 +736,7 @@
$\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no
permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
(similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be
- shown that all three notions of $\alpha$-equivalence coincide, if we only
+ shown that all three notions of alpha-equivalence coincide, if we only
abstract a single atom.
In the rest of this section we are going to introduce three abstraction
@@ -756,12 +751,12 @@
and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
relations. %% and equivariant.
- \begin{lemma}\label{alphaeq}
+ \begin{lem}\label{alphaeq}
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations. %, and if
%@{term "abs_set (as, x) (bs, y)"} then also
%@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
- \end{lemma}
+ \end{lem}
\begin{proof}
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
@@ -774,7 +769,7 @@
\noindent
This lemma allows us to use our quotient package for introducing
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_set+"} and @{text "\<beta> abs_list"}
- representing $\alpha$-equivalence classes of pairs of type
+ representing alpha-equivalence classes of pairs of type
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}
(in the third case).
The elements in these types will be, respectively, written as
@@ -791,7 +786,7 @@
\emph{abstractions}. The important property we need to derive is the support of
abstractions, namely:
- \begin{theorem}[Support of Abstractions]\label{suppabs}
+ \begin{thm}[Support of Abstractions]\label{suppabs}
Assuming @{text x} has finite support, then
\begin{center}
@@ -802,7 +797,7 @@
@{thm (rhs) supp_Abs(3)[where bs="bs", no_vars]}
\end{tabular}
\end{center}
- \end{theorem}
+ \end{thm}
\noindent
This theorem states that the bound names do not appear in the support.
@@ -828,13 +823,13 @@
\noindent
The second fact derives from the definition of permutations acting on pairs
- \eqref{permute} and $\alpha$-equivalence being equivariant
+ \eqref{permute} and alpha-equivalence being equivariant
(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
the following lemma about swapping two atoms in an abstraction.
- \begin{lemma}
+ \begin{lem}
@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
- \end{lemma}
+ \end{lem}
\begin{proof}
This lemma is straightforward using \eqref{abseqiff} and observing that
@@ -886,7 +881,7 @@
properties about them. It would be
laborious to write custom ML-code that derives automatically such properties
for every term-constructor that binds some atoms. Also the generality of
- the definitions for $\alpha$-equivalence will help us in the next sections.
+ the definitions for alpha-equivalence will help us in the next sections.
*}
section {* Specifying General Bindings\label{sec:spec} *}
@@ -905,7 +900,7 @@
\mbox{\begin{tabular}{@ {}p{2.5cm}l}
type \mbox{declaration part} &
$\begin{cases}
- \mbox{\small\begin{tabular}{l}
+ \mbox{\begin{tabular}{l}
\isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
\isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
\raisebox{2mm}{$\ldots$}\\[-2mm]
@@ -914,7 +909,7 @@
\end{cases}$\\
binding \mbox{function part} &
$\begin{cases}
- \mbox{\small\begin{tabular}{l}
+ \mbox{\begin{tabular}{l}
\isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
\isacommand{where}\\
\raisebox{2mm}{$\ldots$}\\[-2mm]
@@ -961,7 +956,7 @@
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). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
+ preserving alpha-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
clause will be called \emph{bodies}; the
``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to
Ott, we allow multiple labels in binders and bodies.
@@ -983,13 +978,13 @@
Similarly for the other binding modes.
Interestingly, in case of \isacommand{bind (set)}
and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics
- of the specifications (the corresponding $\alpha$-equivalence will differ). We will
+ of the specifications (the corresponding alpha-equivalence will differ). We will
show this later with an example.
There are also some restrictions we need to impose on our binding clauses in comparison to
the ones of Ott. The
main idea behind these restrictions is that we obtain a sensible notion of
- $\alpha$-equivalence where it is ensured that within a given scope an
+ alpha-equivalence where it is ensured that within a given scope an
atom occurrence cannot be both bound and free at the same time. The first
restriction is that a body can only occur in
\emph{one} binding clause of a term constructor (this ensures that the bound
@@ -1006,7 +1001,7 @@
single name is bound, and type-schemes, where a finite set of names is
bound:
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}}
\begin{tabular}{@ {}l}
\isacommand{nominal\_datatype} @{text lam} $=$\\
@@ -1045,7 +1040,7 @@
tuple patterns might be specified as:
%
\begin{equation}\label{letpat}
- \mbox{\small%
+ \mbox{%
\begin{tabular}{l}
\isacommand{nominal\_datatype} @{text trm} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
@@ -1088,7 +1083,7 @@
specification:
%
\begin{equation}\label{letrecs}
- \mbox{\small%
+ \mbox{%
\begin{tabular}{@ {}l@ {}}
\isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
@@ -1108,13 +1103,13 @@
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 associated
- notions of free-atoms and $\alpha$-equivalence.
+ notions of free-atoms and alpha-equivalence.
To make sure that atoms bound by deep binders cannot be free at the
same time, we cannot have more than one binding function for a deep binder.
Consequently we exclude specifications such as
%
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
@{text "Baz\<^isub>1 p::pat t::trm"} &
\isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\
@@ -1128,10 +1123,10 @@
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
out different atoms to become bound, respectively be free, in @{text "p"}.
(Since the Ott-tool does not derive a reasoning infrastructure for
- $\alpha$-equated terms with deep binders, it can permit such specifications.)
+ alpha-equated terms with deep binders, it can permit such specifications.)
We also need to restrict the form of the binding functions in order
- to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
+ to ensure the @{text "bn"}-functions can be defined for alpha-equated
terms. The main restriction is that we cannot return an atom in a binding function that is also
bound in the corresponding term-constructor. That means in \eqref{letpat}
that the term-constructors @{text PVar} and @{text PTup} may
@@ -1139,7 +1134,7 @@
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
may have a binding clause involving the argument @{text trm} (the only one that
is \emph{not} used in the definition of the binding function). This restriction
- is sufficient for lifting the binding function to $\alpha$-equated terms.
+ is sufficient for lifting the binding function to alpha-equated terms.
In the version of
Nominal Isabelle described here, we also adopted the restriction from the
@@ -1149,7 +1144,7 @@
(case @{text PTup}). This restriction will simplify some automatic definitions and proofs
later on.
- In order to simplify our definitions of free atoms and $\alpha$-equivalence,
+ In order to simplify our definitions of free atoms and alpha-equivalence,
we shall assume specifications
of term-calculi are implicitly \emph{completed}. By this we mean that
for every argument of a term-constructor that is \emph{not}
@@ -1157,7 +1152,7 @@
clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
of the lambda-terms, the completion produces
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
\isacommand{nominal\_datatype} @{text lam} =\\
\hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
@@ -1186,15 +1181,15 @@
result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}.
Therefore we will first
extract ``raw'' datatype definitions from the specification and then define
- explicitly an $\alpha$-equivalence relation over them. We subsequently
- construct the quotient of the datatypes according to our $\alpha$-equivalence.
+ explicitly an alpha-equivalence relation over them. We subsequently
+ construct the quotient of the datatypes according to our alpha-equivalence.
The ``raw'' datatype definition can be obtained by stripping off the
binding clauses and the labels from the types. We also have to invent
new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
given by the user. In our implementation we just use the affix ``@{text "_raw"}''.
But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate
- that a notion is given for $\alpha$-equivalence classes and leave it out
+ that a notion is given for alpha-equivalence classes and leave it out
for the corresponding notion given on the ``raw'' level. So for example
we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
where @{term ty} is the type used in the quotient construction for
@@ -1362,7 +1357,7 @@
"fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
"fa\<^bsub>bn\<^esub>"} as follows:
%
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
@{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
@@ -1401,11 +1396,11 @@
Only in the context of a @{text Let} or @{text "Let_rec"}, where the binding clauses are given, will
some atoms actually become bound. This is a phenomenon that has also been pointed
out in \cite{ott-jfp}. For us this observation is crucial, because we would
- not be able to lift the @{text "bn"}-functions to $\alpha$-equated terms if they act on
+ not be able to lift the @{text "bn"}-functions to alpha-equated terms if they act on
atoms that are bound. In that case, these functions would \emph{not} respect
- $\alpha$-equivalence.
+ alpha-equivalence.
- Next we define the $\alpha$-equivalence relations for the raw types @{text
+ Next we define the alpha-equivalence relations for the raw types @{text
"ty"}$_{1..n}$ from the specification. We write them as
\begin{center}
@@ -1414,7 +1409,7 @@
\noindent
Like with the free-atom functions, we also need to
- define auxiliary $\alpha$-equivalence relations
+ define auxiliary alpha-equivalence relations
\begin{center}
@{text "\<approx>bn\<^isub>"}$_{1..m}$
@@ -1434,10 +1429,10 @@
\end{center}
- The $\alpha$-equivalence relations are defined as inductive predicates
+ The alpha-equivalence relations are defined as inductive predicates
having a single clause for each term-constructor. Assuming a
term-constructor @{text C} is of type @{text ty} and has the binding clauses
- @{term "bc"}$_{1..k}$, then the $\alpha$-equivalence clause has the form
+ @{term "bc"}$_{1..k}$, then the alpha-equivalence clause has the form
\begin{center}
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n \<approx>ty C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
@@ -1454,11 +1449,11 @@
\end{center}
\noindent
- In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this
+ In this binding clause no atom is bound and we only have to alpha-relate the bodies. For this
we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
whereby the labels @{text "d"}$_{1..q}$ refer to arguments @{text "z"}$_{1..n}$ and
respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text "z\<PRIME>"}$_{1..n}$. In order to relate
- two such tuples we define the compound $\alpha$-equivalence relation @{text "R"} as follows
+ two such tuples we define the compound alpha-equivalence relation @{text "R"} as follows
\begin{equation}\label{rempty}
\mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
@@ -1489,10 +1484,10 @@
In this case we define a premise @{text P} using the relation
$\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
$\approx_{\,\textit{set+}}$ and $\approx_{\,\textit{list}}$ for the other
- binding modes). This premise defines $\alpha$-equivalence of two abstractions
+ binding modes). This premise defines alpha-equivalence of two abstractions
involving multiple binders. As above, we first build the tuples @{text "D"} and
@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
- compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}).
+ compound alpha-relation @{text "R"} (shown in \eqref{rempty}).
For $\approx_{\,\textit{set}}$ we also need
a compound free-atom function for the bodies defined as
@@ -1518,13 +1513,13 @@
\end{center}
\noindent
- This premise accounts for $\alpha$-equivalence of the bodies of the binding
+ This premise accounts for alpha-equivalence of the bodies of the binding
clause.
However, in case the binders have non-recursive deep binders, this premise
is not enough:
- we also have to ``propagate'' $\alpha$-equivalence inside the structure of
+ we also have to ``propagate'' alpha-equivalence inside the structure of
these binders. An example is @{text "Let"} where we have to make sure the
- right-hand sides of assignments are $\alpha$-equivalent. For this we use
+ right-hand sides of assignments are alpha-equivalent. For this we use
relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
@@ -1542,7 +1537,7 @@
\end{center}
\noindent
- The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
+ The auxiliary alpha-equivalence relations @{text "\<approx>bn"}$_{1..m}$
in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
\begin{center}
@@ -1551,7 +1546,7 @@
\noindent
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
- then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+ then the corresponding alpha-equivalence clause for @{text "\<approx>bn"} has the form
\begin{center}
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
@@ -1575,7 +1570,7 @@
\end{center}
\noindent
- This completes the definition of $\alpha$-equivalence. As a sanity check, we can show
+ This completes the definition of alpha-equivalence. As a sanity check, we can show
that the premises of empty binding clauses are a special case of the clauses for
non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
for the existentially quantified permutation).
@@ -1584,7 +1579,7 @@
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$ with the following clauses:
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
@@ -1593,7 +1588,7 @@
\end{tabular}
\end{center}
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
@@ -1601,7 +1596,7 @@
\end{tabular}
\end{center}
- \begin{center}\small
+ \begin{center}
\begin{tabular}{@ {}c @ {}}
\infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
@@ -1611,7 +1606,7 @@
\noindent
Note the difference between $\approx_{\textit{assn}}$ and
- $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of
+ $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
the components in an assignment that are \emph{not} bound. This is needed in the
clause for @{text "Let"} (which has
a non-recursive binder).
@@ -1624,20 +1619,20 @@
text {*
Having made all necessary definitions for raw terms, we can start
- with establishing the reasoning infrastructure for the $\alpha$-equated types
+ with establishing the reasoning infrastructure for the alpha-equated types
@{text "ty\<AL>"}$_{1..n}$, that is the types the user originally specified. We sketch
in this section the proofs we need for establishing this infrastructure. One
main point of our work is that we have completely automated these proofs in Isabelle/HOL.
First we establish that the
- $\alpha$-equivalence relations defined in the previous section are
+ alpha-equivalence relations defined in the previous section are
equivalence relations.
- \begin{lemma}\label{equiv}
+ \begin{lem}\label{equiv}
Given the raw types @{text "ty"}$_{1..n}$ and binding functions
@{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and
@{text "\<approx>bn"}$_{1..m}$ are equivalence relations. and equivariant.
- \end{lemma}
+ \end{lem}
\begin{proof}
The proof is by mutual induction over the definitions. The non-trivial
@@ -1648,7 +1643,7 @@
\noindent
We can feed this lemma into our quotient package and obtain new types @{text
- "ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$.
+ "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text "ty"}$_{1..n}$.
We also obtain definitions for the term-constructors @{text
"C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
"C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
@@ -1669,7 +1664,7 @@
\noindent
whenever @{text "C"}$^\alpha$~@{text "\<noteq>"}~@{text "D"}$^\alpha$.
- In order to derive this fact, we use the definition of $\alpha$-equivalence
+ In order to derive this fact, we use the definition of alpha-equivalence
and establish that
\begin{equation}\label{distinctraw}
@@ -1680,7 +1675,7 @@
holds for the corresponding raw term-constructors.
In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
package needs to know that the raw term-constructors @{text "C"} and @{text "D"}
- are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).
+ are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
Assuming, for example, @{text "C"} is of type @{text "ty"} with argument types
@{text "ty"}$_{1..r}$, respectfulness amounts to showing that
@@ -1693,7 +1688,7 @@
"x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
@{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this
- implication by applying the corresponding rule in our $\alpha$-equivalence
+ implication by applying the corresponding rule in our alpha-equivalence
definition and by establishing the following auxiliary implications %facts
%
\begin{equation}\label{fnresp}
@@ -1715,7 +1710,7 @@
any bound atoms. In Ott, in contrast, the user may
define @{text "bn"}$_{1..m}$ so that they return bound
atoms and in this case the third implication is \emph{not} true. A
- result is that the lifting of the corresponding binding functions in Ott to $\alpha$-equated
+ result is that the lifting of the corresponding binding functions in Ott to alpha-equated
terms is impossible.
Having established respectfulness for the raw term-constructors, the
@@ -1728,8 +1723,8 @@
\end{center}
\noindent
- are $\alpha$-equivalent. This gives us conditions when the corresponding
- $\alpha$-equated terms are \emph{equal}, namely
+ are alpha-equivalent. This gives us conditions when the corresponding
+ alpha-equated terms are \emph{equal}, namely
\begin{center}
@{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}.
@@ -1737,13 +1732,13 @@
\noindent
We call these conditions as \emph{quasi-injectivity}. They correspond to
- the premises in our $\alpha$-equivalence relations.
+ the premises in our alpha-equivalence relations.
Next we can lift the permutation
operations defined in \eqref{ceqvt}. In order to make this
lifting to go through, we have to show that the permutation operations are respectful.
This amounts to showing that the
- $\alpha$-equivalence relations are equivariant \cite{HuffmanUrban10}.
+ alpha-equivalence relations are equivariant \cite{HuffmanUrban10}.
, which we already established
in Lemma~\ref{equiv}.
As a result we can add the equations
@@ -1782,7 +1777,7 @@
in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
the recursive arguments of @{text "C\<AL>"}.
- By working now completely on the $\alpha$-equated level, we
+ By working now completely on the alpha-equated level, we
can first show that the free-atom functions and binding functions are
equivariant, namely
@@ -1813,12 +1808,12 @@
Lastly, we can show that the support of
elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$.
This fact is important in a nominal setting, but also provides evidence
- that our notions of free-atoms and $\alpha$-equivalence are correct.
+ that our notions of free-atoms and alpha-equivalence are correct.
- \begin{theorem}
+ \begin{thm}
For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have
@{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}.
- \end{theorem}
+ \end{thm}
\begin{proof}
The proof is by induction. In each case
@@ -1911,7 +1906,7 @@
section {* Strong Induction Principles *}
text {*
- In the previous section we derived induction principles for $\alpha$-equated terms.
+ In the previous section we derived induction principles for alpha-equated terms.
We call such induction principles \emph{weak}, because for a
term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}}
the induction hypothesis requires us to establish the implications \eqref{weakprem}.
@@ -2066,13 +2061,13 @@
\noindent
Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
- $\alpha$-equated terms. We can then prove the following two facts
+ alpha-equated terms. We can then prove the following two facts
- \begin{lemma}\label{permutebn}
+ \begin{lem}\label{permutebn}
Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)}
@{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}.
- \end{lemma}
+ \end{lem}
\begin{proof}
By induction on @{text x}. The equations follow by simple unfolding
@@ -2241,23 +2236,23 @@
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
+ 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 no concrete mathematical result concerning this
- notion of $\alpha$-equivalence. Also the definition for the
+ notion of alpha-equivalence. Also the definition for the
notion of free variables
is work in progress.
Although we were heavily inspired by the syntax of Ott,
- its definition of $\alpha$-equi\-valence is unsuitable for our extension of
+ its definition of alpha-equi\-valence 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
+ 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 Ott's
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
+ for our notion of alpha-equivalence in case of \isacommand{bind (set)} and
\isacommand{bind (set+)}.
Consider the examples
@@ -2305,7 +2300,7 @@
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).
+ 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.
@@ -2313,24 +2308,27 @@
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 (set+)}.
+ alpha-equivalence related to our binding mode \isacommand{bind (set+)}.
The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
has a more operational flavour and calculates a partial (renaming) map.
In this way, the definition can deal with vacuous binders. However, to our
best knowledge, no concrete mathematical result concerning this
- definition of $\alpha$-equivalence has been proved.\\[-7mm]
+ definition of alpha-equivalence has been proved.
*}
section {* Conclusion *}
text {*
+ Telsescopes by de Bruijn (AUTOMATH project does not provide an automatic infrastructure).
+
+
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 new definitions of
- $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
+ alpha-equivalence and automated all necessary proofs in Isabelle/HOL.
To specify general binders we used the specifications from Ott, but extended them
in some places and restricted
- them in others so that they make sense in the context of $\alpha$-equated terms.
+ them in others so that they make sense in the context of alpha-equated terms.
We also introduced two binding modes (set and set+) that do not
exist in Ott.
We have tried out the extension with calculi such as Core-Haskell, type-schemes
@@ -2343,7 +2341,7 @@
{http://isabelle.in.tum.de/nominal/download}.}
We have left out a discussion about how functions can be defined over
- $\alpha$-equated terms involving general binders. In earlier versions of Nominal
+ alpha-equated terms involving general binders. In earlier versions of Nominal
Isabelle 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
@@ -2371,20 +2369,18 @@
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
- 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.
+ 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
- \smallskip
\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 of the Ott-tool.\\[-7mm]
- Stephanie Weirich suggested to separate the subgrammars
- of kinds and types in our Core-Haskell example. \\[-6mm]
+ {\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 of the Ott-tool. Stephanie Weirich
+ suggested to separate the subgrammars of kinds and types in our Core-Haskell
+ example.
*}