--- a/Paper/Paper.thy Wed Mar 24 18:02:33 2010 +0100
+++ b/Paper/Paper.thy Wed Mar 24 19:50:42 2010 +0100
@@ -130,9 +130,8 @@
programming language calculus.
By providing these general binding mechanisms, however, we have to work around
- a problem that has been pointed out by Pottier in \cite{Pottier06} and Cheney in
- \cite{Cheney05}: in
- $\mathtt{let}$-constructs of the form
+ a problem that has been pointed out by Pottier \cite{Pottier06} and Cheney
+ \cite{Cheney05}: in $\mathtt{let}$-constructs of the form
%
\begin{center}
$\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
@@ -533,12 +532,12 @@
inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is
a collection of (possibly mutual recursive) type declarations, say
$ty^\alpha_1$, $ty^\alpha_2$, \ldots $ty^\alpha_n$, and an
- associated collection of binding function declarations, say
- $bn^\alpha_1$, \ldots $bn^\alpha_m$. The syntax in Nominal Isabelle
+ associated collection of binding functions, say
+ $bn^\alpha_1$, \ldots, $bn^\alpha_m$. The syntax in Nominal Isabelle
for such specifications is rougly as follows:
%
\begin{equation}\label{scheme}
- \mbox{\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
+ \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
type \mbox{declaration part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
@@ -564,20 +563,20 @@
Every type declaration $ty^\alpha_i$ consists of a collection of
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 for a term-constructor $C^\alpha$ we might have
+ For example a term-constructor $C^\alpha$ might have
\begin{center}
$C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$
\end{center}
\noindent
- whereby some of the $ty'_k$ (or their type components) are contained in the
- set of $ty^\alpha_i$
- declared in \eqref{scheme}. In this case we will call
- the corresponding argument a \emph{recursive argument}. The labels
- annotated on the types are optional and can be used in the (possibly empty)
- list of \emph{binding clauses}. These clauses indicate the binders and the
- scope of the binders in a term-constructor. They come in three \emph{modes}
+ whereby some of the $ty'_k$ (or their components) are contained in the collection
+ of $ty^\alpha_i$ declared in \eqref{scheme}. In this case we will call the
+ corresponding argument a \emph{recursive argument}. The labels annotated on
+ the types are optional and can be used in the (possibly empty) list of
+ \emph{binding clauses}. These clauses indicate the binders and the scope of
+ the binders in a term-constructor. They come in three \emph{modes}
+
\begin{center}
\begin{tabular}{l}
@@ -588,7 +587,7 @@
\end{center}
\noindent
- The first mode is for binding lists of atoms (the order matters); the second is for sets
+ 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 cardinality does) and the last is for
sets of binders (with vacuous binders preserving alpha-equivalence).
@@ -597,7 +596,7 @@
\isacommand{in}\; {\it another\_label} (similar for the other two modes). The
restriction we impose on shallow binders is that the {\it label} must either
refer to a type that is an atom type or to a type that is a finite set or
- list of an atom type. For example the specifications of lambda-terms, where
+ list of an atom type. For example the specifications for lambda-terms, where
a single name is bound, and type-schemes, where a finite set of names is
bound, use shallow binders (the type \emph{name} is an atom type):
@@ -638,7 +637,7 @@
\isacommand{bind\_set}.
A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
- the atoms in one argument of the term-constructor that can be bound in
+ 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}).
The binding functions are expected to return either a set of atoms
@@ -656,15 +655,15 @@
\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::trm}
\;\;\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
\hspace{5mm}$\mid$ Let\;{\it p::pat}\;{\it trm}\; {\it t::trm}
- \;\;\isacommand{bind\_set} {\it bn(p)} \isacommand{in} {\it t}\\
+ \;\;\isacommand{bind} {\it bn(p)} \isacommand{in} {\it t}\\
\isacommand{and} {\it pat} =\\
\hspace{5mm}\phantom{$\mid$} PNo\\
\hspace{5mm}$\mid$ PVr\;{\it name}\\
\hspace{5mm}$\mid$ PPr\;{\it pat}\;{\it pat}\\
- \isacommand{with} {\it bn::pat $\Rightarrow$ atom set}\\
- \isacommand{where} $bn(\textrm{PNil}) = \varnothing$\\
- \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = \{atom\; x\}$\\
- \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1) \cup bn(p_2)$\\
+ \isacommand{with} {\it bn::pat $\Rightarrow$ atom list}\\
+ \isacommand{where} $bn(\textrm{PNil}) = []$\\
+ \hspace{5mm}$\mid$ $bn(\textrm{PVar}\;x) = [atom\; x]$\\
+ \hspace{5mm}$\mid$ $bn(\textrm{PPrd}\;p_1\;p_2) = bn(p_1)\; @\;bn(p_2)$\\
\end{tabular}
\end{center}
@@ -711,48 +710,115 @@
\noindent
since there is no overlap of binders.
- Now the question is how we can turn specifications into actual type
+ Let us come back one more time to the specification of simultaneous lets.
+ A specification for them looks as follows:
+
+ \begin{center}
+ \begin{tabular}{l}
+ \isacommand{nominal\_datatype} {\it trm} =\\
+ \hspace{5mm}\phantom{$\mid$}\ldots\\
+ \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm}
+ \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\
+ \isacommand{and} {\it assn} =\\
+ \hspace{5mm}\phantom{$\mid$} ANil\\
+ \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\
+ \isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\
+ \isacommand{where} $bn(\textrm{ANil}) = []$\\
+ \hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The intention with this specification is to bind all variables
+ from the assignments inside the body @{text t}. However one might
+ like to consider the variant where the variables are not just
+ bound in @{term t}, but also in the assignments themselves. In
+ this case we need to specify
+
+ \begin{center}
+ \begin{tabular}{l}
+ Let\_rec\;{\it a::assn}\; {\it t::trm}
+ \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
+ \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ where we bind also in @{text a} all the atoms @{text bn} returns. In this
+ case we will say the binder is a \emph{recursive binder}.
+
+ Having dealt with all syntax matters, the problem now is how we can turn
+ specifications into actual type
definitions in Isabelle/HOL and then establish a reasoning infrastructure
- for them? Because of the problem Pottier and Cheney pointed out, we cannot
+ for them. Because of the problem Pottier and Cheney pointed out, we cannot
in general re-arrange arguments of term-constructors so that binders and
- their scopes next to each other, an then use the type constructors
- @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"}. Therefore
+ their bodies next to each other, an then use the type constructors
+ @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section
+ \ref{sec:binders}. Therefore
we will first extract datatype definitions from the specification and
then define an alpha-equiavlence relation over them.
The datatype definition can be obtained by just stripping of the
binding clauses and the labels on the types. We also have to invent
new names for the types, $ty^\alpha$ and term-constructors $C^\alpha$
- given by user. We just use an affix:
+ given by user. We just use an affix like
\begin{center}
$ty^\alpha \mapsto ty\_raw \qquad C^\alpha \mapsto C\_raw$
\end{center}
\noindent
- This definition can be made, provided the usual conditions hold: the
- types must be non-empty and the types in the term-constructors need to
- be, what is called, positive position (see \cite{}). We then take the binding
- functions and define them by primitive recursion over the raw datatypes.
- binding function.
+ The datatype definition can be made, provided the usual conditions hold:
+ the datatypes must be non-empty and they must only occur in positive
+ position (see \cite{}). We then consider the user-specified binding
+ functions and define them by primitive recursion over the raw datatypes.
- The first non-trivial step is to read off from the specification free-variable
- functions. There are two kinds: free-variable functions corresponding to types,
- written $\fv\_ty$, and free-variable functions corresponding to binding functions,
- written $\fv\_bn$. They have to be defined at the same time since there can
- be interdependencies. Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$ and some
- binding clauses, the function $\fv (C\_raw\;x_1 \ldots x_n)$ will be the union
- of the values generated for each argument, say $x_i$, as follows:
+ The first non-trivial step we have to generate free-variable
+ functions from the specifications. The basic idea is to collect
+ all atoms that are not bound, but because of the rather complicated
+ binding mechanisms the details are somewhat involved.
+ There are two kinds of free-variable functions: one corresponds to types,
+ written $\fv\_ty$, and the other corresponds to binding functions,
+ written $\fv\_bn$. They have to be defined at the same time, since there can
+ be dependencies between them.
+
+ Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$, of type $ty$ together with
+ some binding clauses, the function $\fv\_ty (C\_raw\;x_1 \ldots x_n)$ will be
+ the union of the values generated for each argument, say $x_i$ with type $ty_i$.
+ By the binding clause we know whether the argument $x_i$ is a shallow or deep
+ binder and in the latter case also whether it is a recursive or non-recursive
+ of a binder. In these cases we return as value:
\begin{center}
- \begin{tabular}{cp{8cm}}
- $\bullet$ & if it is a shallow binder, then $\varnothing$\\
- $\bullet$ & if it is a deep binder, then $\fv_bn x_i$\\
- $\bullet$ & if
+ \begin{tabular}{cp{7cm}}
+ $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
+ $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
+ $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\
\end{tabular}
\end{center}
+ \noindent
+ The binding clause will also give us whether the argument @{term "x\<^isub>i"} is
+ a body of one or more abstractions. There are two cases: either the
+ corresponding binders are all shallow or there is a single deep binder.
+ In the former case we build the union of all shallow binders; in the
+ later case we just take set or list of atoms the specified binding
+ function returns. Below use @{text "bnds"} to stand for them.
+
+ \begin{center}
+ \begin{tabular}{cp{7cm}}
+ $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
+ $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
+ $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
+ $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
+ $\bullet$ & @{term "{}"} otherwise
+ \end{tabular}
+ \end{center}
+ \noindent
+ If the argument is neither a binder, nor a body, then it is defined as
+ the four clauses above, except that @{text "bnds"} is empty. i.e.~no atoms
+ are abstracted.
*}