nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:f296ef291ca9
+:36aeb97fabb0
 text {*
 %%%  @{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"}
 \end{center}
 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic
 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
 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}
 \begin{boxedminipage}{\linewidth}
 \begin{center}
 %
 \begin{center}
 @{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.
 \begin{property}\label{supppermeq}
 @{thm[mode=IfThen] supp_perm_eq[no_vars]}
 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)}
 @{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}
 \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)}\\
 proof obligation use @{text "q + p"}. All conditions are then by simple
 calculations.
 \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>"}
 (in the third case).
 The elements in these types will be, respectively, written as:
 (possibly empty) list of \emph{binding clauses}, which indicate the binders
 and their scope in a term-constructor.  They come in three \emph{modes}:
 \begin{center}
 \begin{tabular}{l}
-\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
-\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
-\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\
+\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
 \end{tabular}
 \end{center}
 \noindent
 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). As indicated, the ``\isacommand{in}-part'' of a binding
-clause will be called \emph{bodies} (there can be more than one); the
+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:
 \begin{center}
 \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\
 \end{tabular}
 \end{center}
 \noindent
-Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set}
+Similarly for the other binding modes.
-and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
+%Interestingly, in case of \isacommand{bind\_set}
-of the specifications (the corresponding $\alpha$-equivalence will differ). We will
+%and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
-show this later with an example.
+%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
+There are also some restrictions we need to impose on binding clauses: the
-it is ensured that a bound variable cannot be free at the same time.  First, a
+main idea behind these restrictions is that we obtain a sensible notion of
-body can only occur in \emph{one} binding clause of a term constructor (this ensures
+$\alpha$-equivalence where it is ensured that within a given scope a
-that the bound variables of a body cannot be free at the same time by specifying
+variable occurence cannot be bound and free at the same time.  First, a body can only occur in
-an alternative binder for the body). For
+\emph{one} binding clause of a term constructor (this ensures that the bound
-binders we distinguish between \emph{shallow} and \emph{deep} binders.
+variables of a body cannot be free at the same time by specifying an
-Shallow binders are just labels. The restriction we need to impose on them
+alternative binder for the body). For binders we distinguish between
-is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
+\emph{shallow} and \emph{deep} binders.  Shallow binders are just
-labels must either refer to atom types or to sets of atom types; in case of
+labels. The restriction we need to impose on them is that in case of
-\isacommand{bind} the labels must refer to atom types or lists of atom
+\isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
-types. Two examples for the use of shallow binders are the specification of
+refer to atom types or to sets of atom types; in case of \isacommand{bind}
-lambda-terms, where a single name is bound, and type-schemes, where a finite
+the labels must refer to atom types or lists of atom types. Two examples for
-set of names is bound:
+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@ {}}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} @{text lam} $=$\\
 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 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{%
 \begin{tabular}{l}
 \isacommand{nominal\_datatype} @{text trm} =\\
 \noindent
 where the argument of the deep binder is also in the body. We call such
 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@ {}}
 \isacommand{nominal\_datatype}~@{text "trm ="}\\
 \hspace{5mm}\phantom{$\mid$}\ldots\\
 \noindent
 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}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Baz\<^isub>1 p::pat t::trm"} &
 \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\
 \end{tabular}
 \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
 \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 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
 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 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
 clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
 of the lambda-calculus, the completion produces
 specifications into actual type definitions in Isabelle/HOL and then
 establish a reasoning infrastructure for them. As
 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
 binding clauses and the labels from the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are
 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"}
+recursion so that for each term constructor @{text "C"} with the
-we have that
+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
+free-variable functions from the specifications. Given a raw term, these
-"ty\<^isub>1 \<dots> ty\<^isub>n"} derived from a specification, we define the
+functions return sets of atoms. Assuming a nominal datatype
-free-variable functions
+specification as in \eqref{scheme} and its \emph{raw} types @{text "ty"}$_{1..n}$,
+we define the free-variable functions
-\begin{center}
+%
+\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}
 \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.
-For atomic types we define the 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_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
-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}"}.
 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
+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 of the values, @{text v}, calculated by the rules for empty, shallow and
+the union @{text "fv(bc\<^isub>1) \<union> \<dots> \<union> fv(bc\<^isub>k)"} of free variables calculated for
-deep binding clauses:
+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}
+\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_set as"} & @{text "="} & @{text "atoms as"}\\
+@{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\
+\end{tabular}
+\end{center}
+\noindent
+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}"}. Otherwise
+the values, @{text v}, calculated by the rules for each bining clause:
 %
 \begin{equation}\label{deepbinderA}
 \mbox{%
 \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}}
 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\
 is a substantial improvement.
 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
 $\alpha$-equivalence of terms that can be specified in Ott.  This definition is
 rather different from ours, not using any nominal techniques.  To our
 Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for
 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
 representing terms involving bindings. Pottier gives a definition for
 $\alpha$-equivalence, which is similar to our binding mode \isacommand{bind}.

changeset 2343	36aeb97fabb0
parent 2342	f296ef291ca9
child 2344	e90f6a26d74b