--- a/Paper/Paper.thy Tue Jun 29 18:00:59 2010 +0100
+++ b/Paper/Paper.thy Wed Jun 30 16:56:37 2010 +0100
@@ -21,9 +21,9 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
- alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup> _") and
fv ("fv'(_')" [100] 100) and
@@ -46,14 +46,14 @@
%%% @{text "(1, (2, 3))"}
So far, Nominal Isabelle provides a mechanism for constructing
- alpha-equated terms, for example
+ $\alpha$-equated terms, for example
\begin{center}
@{text "t ::= x | t t | \<lambda>x. t"}
\end{center}
\noindent
- where free and bound variables have names. For such alpha-equated terms,
+ 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
@@ -87,7 +87,7 @@
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 following two type-schemes as alpha-equivalent
+ we would like to regard the following two type-schemes as $\alpha$-equivalent
%
\begin{equation}\label{ex1}
@{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"}
@@ -95,14 +95,14 @@
\noindent
but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
- the following two should \emph{not} be alpha-equivalent
+ the following two should \emph{not} be $\alpha$-equivalent
%
\begin{equation}\label{ex2}
@{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"}
\end{equation}
\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}
@@ -111,13 +111,13 @@
\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).
- 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}
@@ -125,9 +125,9 @@
\end{equation}
\noindent
- we might not care in which order the assignments $x = 3$ and $y = 2$ are
- given, but it would be unusual to regard \eqref{one} as alpha-equivalent
- with
+ we might not care in which order the assignments @{text "x = 3"} and
+ \mbox{@{text "y = 2"}} are given, but it would be unusual to regard
+ \eqref{one} as $\alpha$-equivalent with
%
\begin{center}
@{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
@@ -149,7 +149,7 @@
\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
+ we do not want to regard \eqref{two} as $\alpha$-equivalent with
%
\begin{center}
@{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"}
@@ -176,27 +176,26 @@
we represent the @{text "\<LET>"}-constructor by something like
%
\begin{center}
- @{text "\<LET> [x\<^isub>1,\<dots>,x\<^isub>n].s [t\<^isub>1,\<dots>,t\<^isub>n]"}
+ @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s) [t\<^isub>1,\<dots>,t\<^isub>n]"}
\end{center}
\noindent
- where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
- becomes bound in @{text s}. In this representation the term
- \mbox{@{text "\<LET> [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 $\mathtt{let}$s as follows
+ 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}}l}
@{text trm} & @{text "::="} & @{text "\<dots>"}\\
- & @{text "|"} & @{text "\<LET> as::assn s::trm"}\hspace{4mm}
+ & @{text "|"} & @{text "\<LET> as::assn s::trm"}\hspace{4mm}
\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
@{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
- & @{text "|"} & @{text "\<ACONS> name trm assn"}
+ & @{text "|"} & @{text "\<ACONS> name trm assn"}
\end{tabular}
\end{center}
@@ -234,11 +233,11 @@
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
+ 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
+ \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,
+ there is a key difference: working with $\alpha$-equated terms means, for example,
that the two type-schemes
\begin{center}
@@ -246,26 +245,26 @@
\end{center}
\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
the Isabelle/HOL theorem prover is a rather non-trivial task. For every
specification we will need to construct a type 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:
@@ -295,16 +294,16 @@
\noindent
We take as the starting point a definition of raw terms (defined as a
- datatype in Isabelle/HOL); identify then 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
+ datatype in Isabelle/HOL); identify then 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 the property that our relation for alpha-equivalence is
+ in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
indeed 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.
@@ -315,7 +314,7 @@
task. To ease it, we re-implemented in Isabelle/HOL 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}
@@ -326,7 +325,7 @@
\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}
@@ -338,15 +337,15 @@
\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. To sum up, every lifting
+ $\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.
+ infrastructure for $\alpha$-equated terms.
The examples we have in mind where our reasoning infrastructure will be
helpful includes the term language of System @{text "F\<^isub>C"}, also
@@ -359,13 +358,17 @@
about them in a theorem prover would be a major pain. \medskip
\noindent
- {\bf Contributions:} We provide new definitions for when terms
- involving multiple binders are alpha-equivalent. These definitions are
+ {\bf Contributions:} We provide novel definitions for when terms
+ 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 concepts behind our specifications of general binders are taken
+ from the Ott-tool, but we introduce restrictions, and also one extension, so
+ that the specifications make sense for reasoning about $\alpha$-equated terms.
+
\begin{figure}
\begin{boxedminipage}{\linewidth}
@@ -472,7 +475,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:
@@ -504,7 +507,7 @@
While often the support of an object can be relatively easily
described, for example for atoms, products, lists, function applications,
- booleans and permutations as follows\\[-6mm]
+ booleans and permutations as follows
%
\begin{eqnarray}
@{term "supp a"} & = & @{term "{a}"}\\
@@ -517,7 +520,7 @@
\end{eqnarray}
\noindent
- in some cases it can be difficult to characterise the support precisely, and
+ In some cases it can be difficult to characterise the support precisely, and
only an approximation can be established (see \eqref{suppfun} above). Reasoning about
such approximations can be simplified with the notion \emph{supports}, defined
as follows:
@@ -532,7 +535,8 @@
two properties.
\begin{property}\label{supportsprop}
- {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]}\\
+ 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{property}
@@ -546,7 +550,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}\;\;\;
@@ -560,13 +564,13 @@
that
%
\begin{center}
- @{text "x R y"} \;\;implies\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+ @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
\end{center}
Finally, the nominal logic work provides us with general means to rename
binders. While in the older version of Nominal Isabelle, we used extensively
Property~\ref{swapfreshfresh} for renaming single binders, this property
- proved unwieldy for dealing with multiple binders. For such binders the
+ proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
\begin{property}\label{supppermeq}
@@ -592,7 +596,7 @@
Most properties given in this section are described in detail in \cite{HuffmanUrban10}
and of course 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.
*}
@@ -607,62 +611,62 @@
In order to keep our work with deriving the reasoning infrastructure
manageable, we will wherever possible state definitions and perform proofs
- on the user-level of Isabelle/HOL, as opposed to write custom ML-code that
+ on the ``user-level'' of Isabelle/HOL, as opposed to write custom ML-code that
generates them anew for each specification. To that end, we will consider
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs
are intended to represent the abstraction, or binding, of the set of atoms @{text
"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
- vacuous binders.) To answer this, we identify four conditions: {\it i)}
+ @{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-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
variables; moreover there must be a permutation @{text p} such that {\it
- ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
- {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
- say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it iv)}
+ (ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
+ {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
+ say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
requirements {\it i)} to {\it iv)} can be stated formally as follows:
%
\begin{equation}\label{alphaset}
- \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
- & @{term "fv(x) - as = fv(y) - bs"}\\
- @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\
- @{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\
- @{text "\<and>"} & @{term "(p \<bullet> as) = bs"}\\
+ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+ \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
+ @{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+ @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
\end{array}
\end{equation}
\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-variable function @{text "fv"} 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
- the latter case, $R$ will be replaced by equality @{text "="} and we
+ $\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 "fv"} is equal to @{text "supp"}.
The definition in \eqref{alphaset} does not make any distinction between the
- order of abstracted variables. If we want this, then we can define alpha-equivalence
+ order of abstracted variables. 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
%
\begin{equation}\label{alphalist}
- \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
- & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
- \wedge & @{term "(fv(x) - set as) \<sharp>* p"}\\
- \wedge & @{text "(p \<bullet> x) R y"}\\
- \wedge & @{term "(p \<bullet> as) = bs"}\\
+ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fv(x) - (set as) = fv(y) - (set bs)"} & \mbox{\it (i)}\\
+ \wedge & @{term "(fv(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ \wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+ \wedge & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\
\end{array}
\end{equation}
\noindent
- where @{term set} is a function that coerces a list of atoms into a set of atoms.
+ where @{term set} is the function that coerces a list of atoms into a set of atoms.
Now the last clause ensures that the order of the binders matters (since @{text as}
and @{text bs} are lists of atoms).
@@ -671,18 +675,19 @@
condition in \eqref{alphaset}:
%
\begin{equation}\label{alphares}
- \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
- & @{term "fv(x) - as = fv(y) - bs"}\\
- \wedge & @{term "(fv(x) - as) \<sharp>* p"}\\
- \wedge & @{text "(p \<bullet> x) R y"}\\
+ \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+ & @{term "fv(x) - as = fv(y) - bs"} & \mbox{\it (i)}\\
+ \wedge & @{term "(fv(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
+ \wedge & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
\end{array}
\end{equation}
- It might be useful to consider some examples for how these definitions of alpha-equivalence
- pan out in practice.
- For this consider the case of abstracting a set of variables over types (as in type-schemes).
- We set @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we define
+ It might be useful to consider first some examples for how these definitions
+ of $\alpha$-equivalence pan out in practice. For this consider the case of
+ abstracting a set of variables over types (as in type-schemes). We set
+ @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we
+ define
\begin{center}
@{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \<rightarrow> T\<^isub>2) = fv(T\<^isub>1) \<union> fv(T\<^isub>2)"}
@@ -691,19 +696,19 @@
\noindent
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} 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
- $\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} to
+ @{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to
+ $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ 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)"}
+ "([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
since there is no permutation that makes the lists @{text "[x, y]"} and
@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
- unchanged. Another example is @{text "({x}, x)"} $\approx_{\textit{res}}$
+ unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$
@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
- $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no
+ $\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
+ (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be
+ 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
@@ -714,13 +719,13 @@
\end{equation}
\noindent
- (similarly for $\approx_{\textit{abs\_res}}$
- and $\approx_{\textit{abs\_list}}$). We can show that these relations are equivalence
+ (similarly for $\approx_{\,\textit{abs\_res}}$
+ and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
relations and equivariant.
\begin{lemma}\label{alphaeq}
- The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$
- and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term
+ The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
+ and $\approx_{\,\textit{abs\_res}}$ 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}
@@ -736,7 +741,7 @@
\noindent
This lemma allows us to use our quotient package and introduce
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} 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:
@@ -783,9 +788,9 @@
\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.
+ the following lemma about swapping two atoms in an abstraction.
\begin{lemma}
@{thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]}
@@ -845,7 +850,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 section.
+ the definitions for $\alpha$-equivalence will help us in the next section.
*}
section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
@@ -883,7 +888,7 @@
\noindent
Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of
- term-constructors, each of which come with a list of labelled
+ term-constructors, each of which comes with a list of labelled
types that stand for the types of the arguments of the term-constructor.
For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
@@ -918,7 +923,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). The ``\isacommand{in}-part'' of a binding
+ 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
@@ -926,9 +931,9 @@
\begin{center}
\begin{tabular}{@ {}ll@ {}}
- @{text "Foo\<^isub>1 x::name y::name t::lam s::lam"} &
+ @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} &
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\
- @{text "Foo\<^isub>2 x::name y::name t::lam s::lam"} &
+ @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} &
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"},
\isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
\end{tabular}
@@ -937,11 +942,15 @@
\noindent
Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
and \isacommand{bind\_res} 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 some restrictions we need to impose on binding clasues: First, a
- body can only occur in \emph{one} binding clause of a term constructor. For
+ There are some restrictions we need to impose on binding clasues: the main idea behind
+ these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where
+ it is ensured that a bound variable cannot be free at the same time. First, a
+ body can only occur in \emph{one} binding clause of a term constructor (this ensures
+ that the bound variables of a body cannot be free at the same time by specifying
+ an alternative binder for the body). For
binders we distinguish between \emph{shallow} and \emph{deep} binders.
Shallow binders are just labels. The restriction we need to impose on them
is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
@@ -954,14 +963,14 @@
\begin{center}
\begin{tabular}{@ {}cc@ {}}
\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
- \isacommand{nominal\_datatype} @{text lam} =\\
+ \isacommand{nominal\_datatype} @{text lam} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
\hspace{5mm}$\mid$~@{text "App lam lam"}\\
\hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
\hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
- \isacommand{nominal\_datatype}~@{text ty} =\\
+ \isacommand{nominal\_datatype}~@{text ty} $=$\\
\hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
\hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
\isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
@@ -971,18 +980,18 @@
\end{center}
\noindent
+ In these specifications @{text "name"} refers to an atom type, and @{text
+ "fset"} to the type of finite sets.
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 makes 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.
+ difference to the semantics of the specification (which we will define below).
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
the atoms in one argument of the term-constructor, which can be bound in
other arguments and also in the same argument (we will call such binders
- \emph{recursive}, see below). The corresponding binding functions are
+ \emph{recursive}, see below). The binding functions are
expected to return either a set of atoms (for \isacommand{bind\_set} and
\isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can
be defined by primitive recursion over the corresponding type; the equations
@@ -1008,7 +1017,7 @@
\isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
\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)"}\\
+ \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\
\end{tabular}}
\end{equation}
@@ -1056,38 +1065,42 @@
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 define below.
- For this definition, we have to impose some restrictions on deep binders. First,
+ function and $\alpha$-equivalence relation, which we are going to define below.
+
+ To make sure that variables bound by deep binders cannot be free at the
+ same time, we have to impose some restrictions. First,
we cannot have more than one binding function for one binder. So we exclude:
\begin{center}
- \begin{tabular}{ll}
- @{text "Baz p::pat t::trm"} &
+ \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}\\
+ @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} &
+ \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"},
+ \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
\end{tabular}
\end{center}
\noindent
- The reason why we must exclude such specifications is that they cannot be
- represented by the general binders described in Section~\ref{sec:binders}.
-
We also need to restrict the form of the binding functions. As will shortly
become clear, we cannot return an atom in a binding function that is also
bound in the corresponding term-constructor. That means in the example
\eqref{letpat} that the term-constructors @{text PVar} and @{text PTup} may
not have a binding clause (all arguments are used to define @{text "bn"}).
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
- may have binding clause involving the argument @{text t} (the only one that
- is \emph{not} used in the definition of the binding function). In the version of
+ may have a binding clause involving the argument @{text t} (the only one that
+ is \emph{not} used in the definition of the binding function).
+
+ In the version of
Nominal Isabelle described here, we also adopted the restriction from the
Ott-tool that binding functions can only return: the empty set or empty list
(as in case @{text PNil}), a singleton set or singleton list containing an
atom (case @{text PVar}), or unions of atom sets or appended atom lists
- (case @{text PTup}). This restriction will simplify some automatic proofs
+ (case @{text PTup}). This restriction will simplify some automatic definitions and proofs
later on.
In order to simplify our definitions, we shall assume specifications
- of term-calculi are \emph{completed}. By this we mean that
+ of term-calculi are implicitly \emph{completed}. By this we mean that
for every argument of a term-constructor that is \emph{not}
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
@@ -1117,7 +1130,7 @@
term-constructors so that binders and their bodies are next to each other will
result in inadequate representations. Therefore we will first
extract datatype definitions from the specification and then define
- explicitly an alpha-equivalence relation over them.
+ explicitly an $\alpha$-equivalence relation over them.
The datatype definition can be obtained by stripping off the
@@ -1125,7 +1138,7 @@
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 defined over alpha-equivalence classes and leave it out
+ that a notion is defined over $\alpha$-equivalence classes and leave it out
for the corresponding notion defined on the ``raw'' level. So for example
we have
@@ -1150,8 +1163,29 @@
@{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
\end{equation}
- The first non-trivial step we have to perform is the generation of free-variable
- functions from the specifications. For atomic types we define the auxilary
+ The first non-trivial step we have to perform is the generation of
+ free-variable functions from the specifications. Given the raw types @{text
+ "ty\<^isub>1 \<dots> ty\<^isub>n"} derived from a specification, we define the
+ free-variable functions
+
+ \begin{center}
+ @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
+ \end{center}
+
+ \noindent
+ We define them together with auxiliary free-variable functions for
+ the binding functions. Given raw binding functions @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
+
+ \begin{center}
+ @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
+ \end{center}
+
+ \noindent
+ The reason for this setup is that in a deep binder not all atoms have to be
+ bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
+ that calculates those unbound atoms.
+
+ For atomic types we define the auxilary
free variable functions:
\begin{center}
@@ -1167,26 +1201,6 @@
the set of atoms to a set of the generic atom type.
It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
- Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} we define now the
- free-variable functions
-
- \begin{center}
- @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
- \end{center}
-
- \noindent
- We define them together with auxiliary free-variable functions for
- the binding functions. Given binding functions
- @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define
- %
- \begin{center}
- @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
- \end{center}
-
- \noindent
- The reason for this setup is that in a deep binder not all atoms have to be
- bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
- that calculates those unbound atoms.
While the idea behind these free-variable functions is clear (they just
collect all atoms that are not bound), because of our rather complicated
@@ -1247,7 +1261,7 @@
The reason why we only have to treat the empty binding clauses specially in
the definition of @{text "fv_bn"} is that binding functions can only use arguments
that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot
- be lifted to alpha-equated terms.
+ be lifted to $\alpha$-equated terms.
To see how these definitions work in practice, let us reconsider the term-constructors
@@ -1288,7 +1302,7 @@
that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because
we would not be able to lift a @{text "bn"}-function that is defined over
arguments that are either binders or bodies. In that case @{text "bn"} would
- not respect alpha-equivalence. We can also see that
+ not respect $\alpha$-equivalence. We can also see that
%
\begin{equation}\label{bnprop}
@{text "fv_ty x = bn x \<union> fv_bn x"}.
@@ -1297,9 +1311,9 @@
\noindent
holds for any @{text "bn"}-function defined for the type @{text "ty"}.
- Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+ Next we define $\alpha$-equivalence relations 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.
+ we also need to define auxiliary $\alpha$-equivalence relations for the binding functions.
Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
To simplify our definitions we will use the following abbreviations for
relations and free-variable acting on products.
@@ -1312,7 +1326,7 @@
\end{center}
- The relations for alpha-equivalence are inductively defined predicates, whose clauses have
+ The relations for $\alpha$-equivalence are inductively defined predicates, whose clauses have
conclusions of the form
%
\begin{center}
@@ -1375,7 +1389,7 @@
- The alpha-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions
+ The $\alpha$-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions
are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}
and need to generate appropriate premises. We generate first premises according to the first three
rules given above. Only the ``left-over'' pairs @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated
@@ -1427,7 +1441,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. Therefore we have
a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant
@@ -1439,10 +1453,10 @@
text {*
Having made all necessary definitions for raw terms, we can start
- introducing the reasoning infrastructure for the alpha-equated types the
+ introducing the reasoning infrastructure for the $\alpha$-equated types the
user originally specified. We sketch in this section the facts we need for establishing
this reasoning infrastructure. First we have to show that the
- alpha-equivalence relations defined in the previous section are indeed
+ $\alpha$-equivalence relations defined in the previous section are indeed
equivalence relations.
\begin{lemma}\label{equiv}
@@ -1460,7 +1474,7 @@
\noindent
We can feed this lemma into our quotient package and obtain new types @{text
- "ty\<AL>\<^bsub>1..n\<^esub>"} representing alpha-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain
+ "ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain
definitions for the term-constructors @{text
"C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
"C"}$_{1..m}$, and similar definitions for the free-variable functions @{text
@@ -1479,7 +1493,7 @@
\end{equation}
\noindent
- By definition of alpha-equivalence we can show that
+ By definition of $\alpha$-equivalence we can show that
for the raw term-constructors
%
\begin{equation}\label{distinctraw}
@@ -1489,7 +1503,7 @@
\noindent
In order to generate \eqref{distinctalpha} from \eqref{distinctraw}, the quotient
package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"}
- 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 @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
@{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
@@ -1498,7 +1512,7 @@
\end{center}
\noindent
- are alpha-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
+ are $\alpha$-equivalent under the assumption that @{text "x\<^isub>i \<approx>ty\<^isub>i y\<^isub>i"} holds for all recursive arguments
and @{text "x\<^isub>i = y\<^isub>i"} holds for all non-recursive arguments of @{text "C\<^isub>i"}. We can prove this by
analysing the definition of @{text "\<approx>ty"}. For this proof to succeed we have to establish
the following auxiliary fact about binding functions. Given a binding function @{text bn\<^isub>i} defined
@@ -1513,7 +1527,7 @@
Having established respectfulness for every raw term-constructor, the
quotient package is able to automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}.
- In fact we can from now on lift facts from the raw level to the alpha-equated level
+ In fact we can from now on lift facts from the raw level to the $\alpha$-equated level
as long as they contain raw term-constructors only. The
induction principles derived by the datatype package in Isabelle/HOL for the types @{text
"ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
@@ -1540,8 +1554,8 @@
to the term-constructors, also permutation operations. In order to make the
lifting go through,
we have to know that the permutation operations are respectful
- w.r.t.~alpha-equivalence. This amounts to showing that the
- alpha-equivalence relations are equivariant, which we already established
+ w.r.t.~$\alpha$-equivalence. This amounts to showing that the
+ $\alpha$-equivalence relations are equivariant, which we already established
in Lemma~\ref{equiv}. As a result we can establish the equations
\begin{equation}\label{calphaeqvt}
@@ -1580,8 +1594,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>n = C\<^sup>\<alpha> y\<^isub>1 \<dots> y\<^isub>n"}
@@ -1592,7 +1606,7 @@
we have to lift in the next section, we completed
the lifting part of establishing the reasoning infrastructure.
- By working now completely on the alpha-equated level, we can first show that
+ By working now completely on the $\alpha$-equated level, we can first show that
the free-variable functions and binding functions
are equivariant, namely
@@ -1609,7 +1623,7 @@
(using the induction principles we lifted above for the types @{text "ty\<AL>\<^bsub>1..n\<^esub>"}).
Until now we have not yet derived anything about the support of the
- alpha-equated terms. This however will be necessary in order to derive
+ $\alpha$-equated terms. This however will be necessary in order to derive
the strong induction principles in the next section.
Using the equivariance properties in \eqref{ceqvt} we can
show for every term-constructor @{text "C\<^sup>\<alpha>"} that
@@ -1727,7 +1741,7 @@
text {*
In the previous section we were able to provide induction principles that
- allow us to perform structural inductions over alpha-equated terms.
+ allow us to perform structural inductions over $\alpha$-equated terms.
We call such induction principles \emph{weak}, because in case of a term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n"},
the induction hypothesis requires us to establish the implication
%
@@ -1772,7 +1786,7 @@
\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}
Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
@@ -1951,36 +1965,50 @@
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 also no concrete mathematical result concerning this
- notion of alpha-equivalence. A definition for the notion of free variables
+ 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
+ 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
+ sense for our $\alpha$-equated terms. Third, it allows empty types that have no
meaning in a HOL-based theorem prover. We also had to generalise slightly their
binding clauses. In Ott you specify binding clauses with a single body; we
allow more than one. We have to do this, because this makes a difference
- for our notion of alpha-equivalence in case of \isacommand{bind\_set} and
+ 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"}\\
+ \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
+ @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
+ \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t s"}\\
+ @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
+ \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t"},
+ \isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "s"}\\
\end{tabular}
\end{center}
\noindent
- behave differently. To see this, consider the following equations
+ behave differently. In the first term-constructor, we essentially have a single
+ body, which happens to be ``spread'' over two arguments; in the second we have
+ two independent bodies, in which the same variables are bound. As a result we
+ have
+
+ \begin{center}
+ \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+ @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
+ @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
+ @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
+ @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+ \end{tabular}
+ \end{center}
+
+ To see this, consider the following equations
\begin{center}
\begin{tabular}{c}
@@ -2016,14 +2044,14 @@
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 mode \isacommand{bind}.
+ $\alpha$-equivalence, which is similar to our binding mode \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
+ of $\alpha$-equivalence is indeed a equivalence relation, but a complete
reasoning infrastructure is well beyond the purposes of his language.
In a slightly different domain (programming with dependent types), the
paper \cite{Altenkirch10} presents a calculus with a notion of
- alpha-equivalence related to our binding mode \isacommand{bind\_res}.
+ $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
This definition is similar to the one by Pottier, except that it
has a more operational flavour and calculates a partial (renaming) map.
In this way they can handle vacous binders. However, their notion of
@@ -2049,7 +2077,7 @@
{http://isabelle.in.tum.de/nominal/download}.
We have left out a discussion about how functions can be defined over
- alpha-equated terms that involve general binders. In earlier versions of Nominal
+ $\alpha$-equated terms 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
@@ -2092,6 +2120,9 @@
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.
+
+
+ * Conference of Altenkirch *
*}
(*<*)