--- a/Paper/Paper.thy Thu Jul 01 01:53:00 2010 +0100
+++ b/Paper/Paper.thy Thu Jul 01 14:18:36 2010 +0100
@@ -46,7 +46,7 @@
%%% @{text "(1, (2, 3))"}
So far, Nominal Isabelle provides a mechanism for constructing
- $\alpha$-equated terms, for example
+ $\alpha$-equated terms, for example lambda-terms
\begin{center}
@{text "t ::= x | t t | \<lambda>x. t"}
@@ -365,9 +365,9 @@
terms, including properties about support, freshness and equality
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
+ The method behind our specification of general binders is 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.
+ that our specifications make sense for reasoning about $\alpha$-equated terms.
\begin{figure}
@@ -567,9 +567,9 @@
@{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
+ Finally, the nominal logic work provides us with general means for renaming
binders. While in the older version of Nominal Isabelle, we used extensively
- Property~\ref{swapfreshfresh} for renaming single binders, this property
+ Property~\ref{swapfreshfresh} to rename single binders, this property
proved too unwieldy for dealing with multiple binders. For such binders the
following generalisations turned out to be easier to use.
@@ -628,7 +628,7 @@
{\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:
+ requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
@@ -739,7 +739,7 @@
\end{proof}
\noindent
- This lemma allows us to use our quotient package and introduce
+ This lemma allows us to use our quotient package for introducing
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
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>"}
@@ -913,9 +913,9 @@
\begin{center}
\begin{tabular}{l}
- \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
- \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
- \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+ \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+ \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+ \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
\end{tabular}
\end{center}
@@ -923,8 +923,8 @@
The first mode is for binding lists of atoms (the order of binders matters);
the second is for sets of binders (the order does not matter, but the
cardinality does) and the last is for sets of binders (with vacuous binders
- preserving $\alpha$-equivalence). The ``\isacommand{in}-part'' of a binding
- clause will be called \emph{bodies} (there can be more than one); the
+ preserving $\alpha$-equivalence). As indicated, 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. For example we allow
binding clauses of the form:
@@ -940,25 +940,28 @@
\end{center}
\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
- show this later with an example.
+ 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
+ %show this later with an example.
- There are some restrictions we need to impose on binding clauses: 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
- labels must either refer to atom types or to sets of atom types; in case of
- \isacommand{bind} the labels must refer to atom types or lists of atom
- types. Two examples for the use of shallow binders are the specification of
- lambda-terms, where a single name is bound, and type-schemes, where a finite
- set of names is bound:
+ There are also some restrictions we need to impose on binding clauses: 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 a
+ variable occurence cannot be bound and 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 labels must either
+ refer to atom types or to sets of atom types; in case of \isacommand{bind}
+ the labels must refer to atom types or lists of atom types. Two examples for
+ the use of shallow binders are the specification of lambda-terms, where a
+ single name is bound, and type-schemes, where a finite set of names is
+ bound:
+
\begin{center}
\begin{tabular}{@ {}cc@ {}}
@@ -994,11 +997,10 @@
\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
+ be defined by recursion over the corresponding type; the equations
must be given in the binding function part of the scheme shown in
\eqref{scheme}. For example a term-calculus containing @{text "Let"}s with
tuple patterns might be specified as:
-
%
\begin{equation}\label{letpat}
\mbox{%
@@ -1042,7 +1044,7 @@
binders \emph{recursive}. To see the purpose of such recursive binders,
compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following
specification:
-
+ %
\begin{equation}\label{letrecs}
\mbox{%
\begin{tabular}{@ {}l@ {}}
@@ -1065,10 +1067,10 @@
The difference is that with @{text Let} we only want to bind the atoms @{text
"bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms
inside the assignment. This difference has consequences for the free-variable
- function and $\alpha$-equivalence relation, which we are going to define below.
+ function and $\alpha$-equivalence relation, which we are going to define later.
To make sure that variables bound by deep binders cannot be free at the
- same time, we have to impose some restrictions. First,
+ same time, we have to impose some further restrictions. First,
we cannot have more than one binding function for one binder. So we exclude:
\begin{center}
@@ -1082,6 +1084,10 @@
\end{center}
\noindent
+ Otherwise it is be possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
+ out different atoms to become bound in @{text "p"}.
+
+
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
@@ -1089,7 +1095,8 @@
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 a binding clause involving the argument @{text t} (the only one that
- is \emph{not} used in the definition of the binding function).
+ is \emph{not} used in the definition of the binding function). This restriction
+ means that we can lift the binding function to $\alpha$-equated terms.
In the version of
Nominal Isabelle described here, we also adopted the restriction from the
@@ -1099,7 +1106,8 @@
(case @{text PTup}). This restriction will simplify some automatic definitions and proofs
later on.
- In order to simplify our definitions, we shall assume specifications
+ In order to simplify our definitions of free variables 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}
already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding
@@ -1132,9 +1140,11 @@
Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just
re-arranging the arguments of
term-constructors so that binders and their bodies are next to each other will
- result in inadequate representations. Therefore we will first
+ 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 datatype definitions from the specification and then define
- explicitly an $\alpha$-equivalence relation over them.
+ explicitly an $\alpha$-equivalence relation over them. We subsequently
+ quotient the datatypes according to our $\alpha$-equivalence.
The datatype definition can be obtained by stripping off the
@@ -1158,28 +1168,33 @@
non-empty and the types in the constructors only occur in positive
position (see \cite{Berghofer99} for an indepth description of the datatype package
in Isabelle/HOL). We then define the user-specified binding
- functions, called @{term "bn"}, by primitive recursion over the corresponding
+ functions, called @{term "bn"}, by recursion over the corresponding
raw datatype. We can also easily define permutation operations by
- primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}
- we have that
+ recursion so that for each term constructor @{text "C"} with the
+ argument types @{text "ty"}$_{1..n}$ we have that
%
\begin{equation}\label{ceqvt}
@{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}
+
+ \noindent
+ where the variables @{text "z"}$_{1..n}$ are of types @{text "ty"}$_{1..n}$.
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}
+ free-variable functions from the specifications. Given a raw term, these
+ functions return sets of atoms. Assuming a nominal datatype
+ specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$,
+ we define the free-variable functions
+ %
+ \begin{equation}\label{fvars}
@{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
- \end{center}
+ \end{equation}
\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
-
+ the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
+ we define
+ %
\begin{center}
@{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
\end{center}
@@ -1187,32 +1202,65 @@
\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.
+ that calculates those unbound atoms in a deep binder.
+
+ While the idea behind these free-variable functions is clear (they just
+ collect all atoms that are not bound), because of our rather complicated
+ binding mechanisms their definitions are somewhat involved. Given a
+ term-constructor @{text "C"} of type @{text ty} and some associated binding
+ clauses @{text "bc\<^isub>1\<dots>bc\<^isub>k"}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
+ the union @{text "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} of free variables calculated for
+ each binding clause. Given a binding clause @{text bc} is of the form
+ %
+ \begin{equation}
+ \mbox{\isacommand{bind} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+ \end{equation}
- For atomic types we define the auxiliary
- free variable functions:
+ \noindent
+ where the body labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$; the binders
+ @{text b}$_{1..p}$
+ either refer to labels of atom types (in case of shallow binders) or to binding
+ functions taking a single label as argument (in case of deep binders). Assuming the
+ free variables of the bodies is the set @{text "D"}, the bound variables of the binders
+ is the set @{text B} and the free variables of the non-recursive deep binders is @{text "B'"}
+ then the free variables of the binding clause @{text bc} is
+ %
+ \begin{center}
+ @{text "fv(bc) = (D - B) \<union> B'"}
+ \end{center}
+
+ \noindent
+ Formally the set @{text D} is the union of the free variables for the bodies
+ %
+ \begin{center}
+ @{text "D = fv_ty\<^isub>1 d\<^isub>1 \<union> ... \<union> fv_ty\<^isub>q d\<^isub>q"}
+ \end{center}
+
+ \noindent
+ whereby the free variable functions @{text "fv_ty\<^isub>i"} are the ones in \eqref{fvars}
+ provided the @{text "d\<^isub>i"} refers to one of the types @{text "ty"}$_{1..n}$;
+ otherwise we set @{text "fv_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+
+
+if @{text "d\<^isub>i"} is a label
+ for an atomic type we use the following auxiliary free variable functions
\begin{center}
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\
+ @{text "fv_atom a"} & @{text "="} & @{text "{atom a}"}\\
@{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\
@{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
\end{tabular}
\end{center}
\noindent
- Like the coercion function @{text atom}, @{text "atoms"} coerces
+ In these functions, @{text "atoms"}, like @{text "atom"}, coerces
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}"}.
+ It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}. Otherwise
+
- While the idea behind these free-variable functions is clear (they just
- collect all atoms that are not bound), because of our rather complicated
- binding mechanisms their definitions are somewhat involved. Given a
- term-constructor @{text "C"} of type @{text ty} and some associated binding
- clauses @{text bcs}, the result of the @{text "fv_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be
- the union of the values, @{text v}, calculated by the rules for empty, shallow and
- deep binding clauses:
+the values, @{text v}, calculated by the rules for each bining clause:
%
\begin{equation}\label{deepbinderA}
\mbox{%
@@ -1965,7 +2013,7 @@
The most closely related work to the one presented here is the Ott-tool
\cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
front-end for creating \LaTeX{} documents from specifications of
- term-calculi involving general binders. For a subset of the specifications,
+ term-calculi involving general binders. For a subset of the specifications
Ott can also generate theorem prover code using a raw representation of
terms, and in Coq also a locally nameless representation. The developers of
this tool have also put forward (on paper) a definition for
@@ -2043,7 +2091,7 @@
representing terms with general binders inside OCaml. This language is
implemented as a front-end that can be translated to OCaml with a help of
a library. He presents a type-system in which the scope of general binders
- can be indicated with some special constructs, written @{text "inner"} and
+ can be indicated with some special markers, written @{text "inner"} and
@{text "outer"}. With this, it seems, our and his specifications can be
inter-translated, but we have not proved this. However, we believe the
binding specifications in the style of Ott are a more natural way for