--- a/Paper/Paper.thy Tue Mar 23 13:07:11 2010 +0100
+++ b/Paper/Paper.thy Tue Mar 23 17:22:19 2010 +0100
@@ -130,7 +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}: in
+ a problem that has been pointed out by Pottier in \cite{Pottier06} and Cheney in
+ \cite{Cheney05}: in
$\mathtt{let}$-constructs of the form
%
\begin{center}
@@ -150,7 +151,7 @@
\noindent
where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound
in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
- would be a perfectly legal instance. To exclude such terms an additional
+ would be a perfectly legal instance. To exclude such terms, an additional
predicate about well-formed terms is needed in order to ensure that the two
lists are of equal length. This can result into very messy reasoning (see
for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
@@ -182,17 +183,18 @@
heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}.
However, we will not be able to deal with all specifications that are
- allowed by Ott. One reason is that Ott allows ``empty'' specifications
- like
+ allowed by Ott. One reason is that Ott lets the user to specify ``empty''
+ types like
\begin{center}
$t ::= t\;t \mid \lambda x. t$
\end{center}
\noindent
- where no clause for variables is given. 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.
+ 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.
Another reason is that we establish the reasoning infrastructure
for alpha-\emph{equated} terms. In contrast, Ott produces a reasoning
@@ -200,14 +202,14 @@
\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 that the
- two type-schemes with $x$, $y$ and $z$ being distinct
+ two type-schemes (with $x$, $y$ and $z$ being distinct)
\begin{center}
$\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$
\end{center}
\noindent
- are not just alpha-equal, but actually equal. As a
+ 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
@@ -264,7 +266,7 @@
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 in the representation of terms using the locally
+ 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.
@@ -273,10 +275,10 @@
a reasoning infrastructure needs to be ``lifted'' from the underlying subset to
the new type. This is usually a tricky and arduous task. To ease it,
we re-implemented in Isabelle/HOL the quotient package described by Homeier
- \cite{Homeier05}. This package
+ \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 define the free-variable function over lambda terms
+ to definitions and theorems involving alpha-equated terms. For example
+ if we define the free-variable function over raw lambda-terms
\begin{center}
$\fv(x) = \{x\}$\hspace{10mm}
@@ -286,7 +288,8 @@
\noindent
then with not too great effort we obtain a function $\fv_\alpha$
- operating on quotients, or alpha-equivalence classes of terms, as follows
+ 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}
@@ -297,8 +300,8 @@
\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 an equivalence relation, and the
- definitions and theorems are respectful w.r.t.~alpha-equivalence. Hence we
+ only works if alpha-equivalence is an equivalence relation, and the lifted
+ definitions and theorems are respectful w.r.t.~alpha-equivalence. Accordingly, we
will not be able to lift a bound-variable function to alpha-equated terms
(since it does not respect alpha-equivalence). To sum up, every lifting of
theorems to the quotient level needs proofs of some respectfulness
@@ -329,23 +332,27 @@
represent different kinds of variables, such as term- and type-variables in
Core-Haskell, and it is assumed that there is an infinite supply of atoms
for each sort. However, in order to simplify the description, we shall
- assume in what follows that there is only a single sort of atoms.
-
+ assume in what follows that there is only one sort of atoms.
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
-
- @{text[display,indent=5] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ %
+ @{text[display,indent=5] "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
\noindent
- with a generic type in which @{text "\<alpha>"} stands for the type of atoms
- and @{text "\<beta>"} for the type of the object on which the permutation
- acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},
+ with a generic type in which @{text "\<beta>"} stands for the type of the object
+ on which the permutation
+ acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}
and the inverse permutation of @{term p} as @{text "- p"}. The permutation
operation is defined for products, lists, sets, functions, booleans etc
- (see \cite{HuffmanUrban10}).
+ (see \cite{HuffmanUrban10}). In the nominal logic work, concrete
+ permutations are usually build up from swappings, written as @{text "(a b)"},
+ which are permutations that behave as follows:
+ %
+ @{text[display,indent=5] "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
+
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
@@ -354,13 +361,13 @@
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:
-
+ %
@{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
\noindent
There is also the derived notion for when an atom @{text a} is \emph{fresh}
for an @{text x}, defined as
-
+ %
@{thm[display,indent=5] fresh_def[no_vars]}
\noindent
@@ -391,34 +398,34 @@
text {*
In Nominal Isabelle, the user is expected to write down a specification of a
term-calculus and then a reasoning infrastructure is automatically derived
- from this specifcation (remember that Nominal Isabelle is a definitional
+ from this specification (remember that Nominal Isabelle is a definitional
extension of Isabelle/HOL, which does not introduce any new axioms).
In order to keep our work manageable, we will wherever possible state
definitions and perform proofs inside Isabelle, as opposed to write custom
- ML-code that generates them for each instance of a term-calculus. To that
+ ML-code that generates them anew for each specification. To that
end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
- These pairs are intended to represent the abstraction, or binding, of the set $as$
- in the body $x$.
+ These pairs are intended to represent the abstraction, or binding, of the set @{text "as"}
+ in the body @{text "x"}.
The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
alpha-equivalent? (At 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)} given
- a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
- need to have the same set of free variables; moreover there must be a permutation,
- $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged,
- but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation,
- say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes
- the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can
+ a free-variable function $\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)} it 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 equal terms. We also require {\it iv)} that @{text p} makes
+ the abstracted sets @{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}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - as = fv(y) - bs"}\\
- \wedge & @{text "fv(x) - as #* p"}\\
+ \wedge & @{text "(fv(x) - as) #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
\wedge & @{text "(p \<bullet> as) = bs"}\\
\end{array}
@@ -431,8 +438,7 @@
$R$. The reason for this extra generality is that we will use $\approx_{set}$ for both
``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by
equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support
- of $x$ and $y$. To have these parameters means, however, we can derive properties about
- them generically.
+ of $x$ and $y$.
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
@@ -443,14 +449,14 @@
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
\multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
- \wedge & @{text "fv(x) - (set as) #* p"}\\
+ \wedge & @{text "(fv(x) - set as) #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
\wedge & @{text "(p \<bullet> as) = bs"}\\
\end{array}
\end{equation}
\noindent
- where $set$ is just the function that coerces a list of atoms into a set of atoms.
+ where $set$ is the function that coerces a list of atoms into a set of atoms.
If we do not want to make any difference between the order of binders and
also allow vacuous binders, then we keep sets of binders, but drop the fourth
@@ -460,7 +466,7 @@
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
\multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
& @{text "fv(x) - as = fv(y) - bs"}\\
- \wedge & @{text "fv(x) - as #* p"}\\
+ \wedge & @{text "(fv(x) - as) #* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
\end{array}
\end{equation}
@@ -478,12 +484,13 @@
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 equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
- be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then
+ be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then
$([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
- makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the
- type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
- $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
- However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
+ makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the
+ type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another examples is
+ $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ which holds by taking $p$ to be the identity permutation.
+ However, if @{text "x \<noteq> y"}, then
+ $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
\end{exmple}
@@ -522,17 +529,17 @@
section {* Alpha-Equivalence and Free Variables *}
text {*
- The syntax of a specification for a term-calculus in Nominal Isabelle is
- heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a
- collection of (possibly mutual recursive) type declarations, say
- $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
- collection of associated binding function declarations, say
- $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically
- written as follows:
+ 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
+ associated collection of binding function declarations, say
+ $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as
+ follows:
\begin{center}
\begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
- types \mbox{declaration part} &
+ type \mbox{declaration part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
\isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\
@@ -541,7 +548,7 @@
\isacommand{and} $ty_{\alpha{}n} = \ldots$\\
\end{tabular}}
\end{cases}$\\
- binding \mbox{functions part} &
+ binding \mbox{function part} &
$\begin{cases}
\mbox{\begin{tabular}{l}
\isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$
@@ -554,31 +561,36 @@
\end{center}
\noindent
- Each 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,
- like
+ types that indicate 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}$
\end{center}
\noindent
- The labels are optional and can be used in the (possibly empty) list of binding clauses.
- These clauses indicate the binders and the scope of the binders in a term-constructor. They
- are of the form
+ 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
\begin{center}
- \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}
+ \begin{tabular}{l}
+ \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+ \end{tabular}
\end{center}
\noindent
- whereby we distinguish between \emph{shallow} binders and \emph{deep} binders.
- Shallow binders are just of the form \isacommand{bind}\; {\it label}\;
- \isacommand{in}\; {\it another\_label}. The only restriction on shallow binders
- is that the {\it label} must refer to either a type which is single atom or
- to a type which is a finite set of atoms. For example the specification of
- lambda-terms and type-schemes use them:
+ 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):
\begin{center}
\begin{tabular}{@ {}cc@ {}}
@@ -587,20 +599,36 @@
\hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
\hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
\hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
- \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+ \hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
\end{tabular} &
\begin{tabular}{@ {}l@ {}}
\isacommand{nominal\_datatype} {\it ty} =\\
\hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
\hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
- \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
- \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\
+ \isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
+ \hspace{22mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
\end{tabular}
\end{tabular}
\end{center}
\noindent
- A specification of a term-calculus in Nominal Isabell is very similar to
+ A \emph{deep} binder uses an auxiliary binding function that picks out the atoms
+ that are bound in one or more arguments. This binding function returns either
+ a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a
+ list of atoms (for \isacommand{bind}). Such binding functions can be defined
+ by primitive recursion over the corresponding type. They are defined by equations
+ included in the binding function part of the scheme given above.
+
+ For the moment we
+ adopt the restriction of the Ott-tool that binding functions can only return
+ the empty set, a singleton set of atoms or unions of atom sets. For example
+
+ over the type for which they specify the bound atoms.
+
+
+
+ \noindent
+ A specification of a term-calculus in Nominal Isabelle is very similar to
the usual datatype definition of Isabelle/HOL: