# HG changeset patch # User Cezary Kaliszyk # Date 1269428643 -3600 # Node ID 9db725590fe932b33578493b522d0d26db19c9fb # Parent 0d7d0b8adca56ae09dfe1e60d37e2b120a208ec8# Parent 17a2c6fddc0c15f3916b3a340234eee1b36826b7 merge diff -r 0d7d0b8adca5 -r 9db725590fe9 Paper/Paper.thy --- a/Paper/Paper.thy Wed Mar 24 12:03:48 2010 +0100 +++ b/Paper/Paper.thy Wed Mar 24 12:04:03 2010 +0100 @@ -287,14 +287,14 @@ \end{center} \noindent - then with not too great effort we obtain a function $\fv_\alpha$ + then with not too great effort we obtain a function $\fv^\alpha$ operating on quotients, or alpha-equivalence classes of lambda-terms. This function is characterised by the equations \begin{center} - $\fv_\alpha(x) = \{x\}$\hspace{10mm} - $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm] - $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$ + $\fv^\alpha(x) = \{x\}$\hspace{10mm} + $\fv^\alpha(t_1\;t_2) = \fv^\alpha(t_1) \cup \fv^\alpha(t_2)$\\[1mm] + $\fv^\alpha(\lambda x.t) = \fv^\alpha(t) - \{x\}$ \end{center} \noindent @@ -393,7 +393,7 @@ *} -section {* General Binders *} +section {* General Binders\label{sec:binders} *} text {* In Nominal Isabelle, the user is expected to write down a specification of a @@ -532,26 +532,26 @@ Our specifications for term-calculi are heavily 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 + $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}$. They are schematically written as - follows: + $bn^\alpha_1$, \ldots $bn^\alpha_m$. The syntax for a specification is + rougly as follows: \begin{equation}\label{scheme} \mbox{\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l} type \mbox{declaration part} & $\begin{cases} \mbox{\begin{tabular}{l} - \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\ - \isacommand{and} $ty_{\alpha{}2} = \ldots$\\ + \isacommand{nominal\_datatype} $ty^\alpha_1 = \ldots$\\ + \isacommand{and} $ty^\alpha_2 = \ldots$\\ $\ldots$\\ - \isacommand{and} $ty_{\alpha{}n} = \ldots$\\ + \isacommand{and} $ty^\alpha_n = \ldots$\\ \end{tabular}} \end{cases}$\\ binding \mbox{function part} & $\begin{cases} \mbox{\begin{tabular}{l} - \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$ + \isacommand{with} $bn^\alpha_1$ \isacommand{and} \ldots \isacommand{and} $bn^\alpha_m$ $\ldots$\\ \isacommand{where}\\ $\ldots$\\ @@ -561,19 +561,22 @@ \end{equation} \noindent - Every type declaration $ty_{\alpha{}i}$ consists of a collection of + Every type declaration $ty^\alpha_i$ consists of a collection of term-constructors, each of which comes with a list of labelled - types that indicate the types of the arguments of the term-constructor. - For example for a term-constructor $C_{\alpha}$ we might have + types that stand for the types of the arguments of the term-constructor. + For example for a term-constructor $C^\alpha$ we might have \begin{center} - $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$ + $C^\alpha\;label_1\!::\!ty'_1\;\ldots label_l\!::\!ty'_l\;\;\textit{binding\_clauses}$ \end{center} \noindent - The labels 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 forms + whereby some of the $ty'_k$ 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} \begin{center} \begin{tabular}{l} @@ -584,13 +587,18 @@ \end{center} \noindent - whereby we also distinguish between \emph{shallow} binders and \emph{deep} binders. - Shallow binders are of the form \isacommand{bind}\; {\it label}\; - \isacommand{in}\; {\it another\_label} (similar the other forms). 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 and type-schemes use shallow binders (where \emph{name} is an atom type): + The first mode is for binding lists of atoms (order matters); in the second sets + of binders (order does not matter, but cardinality does) and in the last + sets of binders (with vacuous binders preserving alpha-equivalence). + + In addition we distinguish between \emph{shallow} binders and \emph{deep} + binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\; + \isacommand{in}\; {\it another\_label} (similar 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 + 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): \begin{center} \begin{tabular}{@ {}cc@ {}} @@ -612,17 +620,37 @@ \end{center} \noindent - A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms - in one argument that can be bound in one or more arguments. Such a binding function returns either - a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a - list of atoms (for \isacommand{bind}). It can be defined - by primitive recursion over the corresponding type; the equations - are stated in the binding function part of the scheme shown in \eqref{scheme}. + If we have shallow binders that ``share'' a body, for example + + \begin{center} + \begin{tabular}{ll} + \it {\rm Foo}$_0$ x::name y::name t::lam & \it + \isacommand{bind}\;x\;\isacommand{in}\;t,\; + \isacommand{bind}\;y\;\isacommand{in}\;t + \end{tabular} + \end{center} + + \noindent + then we have to make sure the modes of the binders agree. For example we cannot + have in the first binding clause the mode \isacommand{bind} and in the second + \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 one + or more of the other arguments and also can be bound in the same argument (we will + call such binders \emph{recursive}). + 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 must be given in the binding function part of + the scheme shown in \eqref{scheme}. + In the present version of Nominal Isabelle, we adopted the restrictions the Ott-tool imposes on the binding functions, namely a - binding functions can only return the empty set, a singleton set of atoms or - unions of atom sets. For example for lets with patterns you might define + binding function can only return the empty set, a singleton set containing an + atom or unions of atom sets. For example for lets with tuple patterns you might + define \begin{center} \begin{tabular}{l} @@ -645,10 +673,44 @@ \end{center} \noindent - In this definition the function $atom$ coerces a name into the generic - atom type of Nominal Isabelle. In this way we can treat binders of different - type uniformely. + In this specification the function $atom$ coerces a name into the generic + atom type of Nominal Isabelle. This allows us to treat binders of different + type uniformly. As will shortly become clear, we cannot return an atom + in a binding function that also is bound in the term-constructor. + + Like with shallow binders, deep binders with shared body need to have the + same binding mode. A more serious restriction we have to impose on deep binders + is that we cannot have ``overlapping'' binders. Consider for example the + term-constructors: + \begin{center} + \begin{tabular}{ll} + \it {\rm Foo}$_1$ p::pat q::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\; + \isacommand{bind}\;bn(q)\;\isacommand{in}\;t\\ + \it {\rm Foo}$_2$ x::name p::pat t::trm & \it \it \isacommand{bind}\;x\;\isacommand{in}\;t,\; + \isacommand{bind}\;bn(p)\;\isacommand{in}\;t + + \end{tabular} + \end{center} + + \noindent + In the first case we bind all atoms from the pattern $p$ in $t$ and also all atoms + from $q$ in $t$. Therefore the binders overlap in $t$. Similarly in the second case: + the binder $bn(p)$ overlap with the shallow binder $x$. We must exclude such specifiactions, + as we will not be able to represent them using the general binders described in + Section \ref{sec:binders}. However the following two term-constructors are allowed: + + \begin{center} + \begin{tabular}{ll} + \it {\rm Bar}$_1$ p::pat t::trm s::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;t,\; + \isacommand{bind}\;bn(p)\;\isacommand{in}\;s\\ + \it {\rm Bar}$_2$ p::pat t::trm & \it \isacommand{bind}\;bn(p)\;\isacommand{in}\;p,\; + \isacommand{bind}\;bn(p)\;\isacommand{in}\;t\\ + \end{tabular} + \end{center} + + \noindent + as no overlapping of binders occurs. Because of the problem Pottier pointed out in \cite{Pottier06}, the general