nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:fbdaaa20396b
+:1c18f2cf3923
 The scope of the binding is indicated by labels given to the types, for
 example @{text "s::trm"}, and a binding clause, in this case
 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
 clause states that all the names the function @{text
 "bn(as)"} returns should be bound in @{text s}.  This style of specifying terms and bindings is heavily
-inspired by the syntax of the Ott-tool \cite{ott-jfp}.
+inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott
+has only one binding mode, namely the one where the order of
+binders matters. Consequently, type-schemes with binding sets
+of names cannot be modelled in Ott.
 However, we will not be able to cope with all specifications that are
 allowed by Ott. One reason is that Ott lets the user specify ``empty''
 types like
 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 method behind our specification of general binders is taken
 from the Ott-tool, but we introduce crucial restrictions, and also extensions, so
-that our specifications make sense for reasoning about $\alpha$-equated terms.
+that our specifications make sense for reasoning about $\alpha$-equated terms.  The main improvement over Ott is that we introduce three binding modes,
+provide precise definitions for $\alpha$-equivalence and for free
+variables of our terms, and provide automated proofs inside the
+Isabelle theorem prover.
 \begin{figure}
 \begin{boxedminipage}{\linewidth}
 \begin{center}
 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 bodies}\\
-\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+\isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
-\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+\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);
 \end{tabular}
 \end{center}
 \noindent
 Similarly for the other binding modes.
-%Interestingly, in case of \isacommand{bind\_set}
+%Interestingly, in case of \isacommand{bind (set)}
-%and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics
+%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 also some restrictions we need to impose on our binding clauses in comparison to
 the ones of Ott. The
 \emph{one} binding clause of a term constructor (this ensures that the bound
 atoms of a body cannot be free at the same time by specifying an
 alternative binder for the same 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
+\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@ {}}
-\begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+\begin{tabular}{@ {}l@ {\hspace{-2mm}}}
 \isacommand{nominal\_datatype} @{text lam} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
 \hspace{5mm}$\mid$~@{text "App lam lam"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"}\\
 \hspace{21mm}\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype}~@{text ty} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\
 \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\
 \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\\
-\hspace{24mm}\isacommand{bind\_res} @{text xs} \isacommand{in} @{text T}\\
+\hspace{21mm}\isacommand{bind (res)} @{text xs} \isacommand{in} @{text T}\\
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
 In these specifications @{text "name"} refers to an atom type, and @{text
 "fset"} to the type of finite sets.
 Note that for @{text lam} it does not matter which binding mode we use. The
 reason is that we bind only a single @{text name}. However, having
-\isacommand{bind\_set} or \isacommand{bind} in the second case makes a
+\isacommand{bind (set)} or \isacommand{bind} in the second case makes a
 difference to the semantics of the specification (which we will define in the next section).
 A \emph{deep} binder uses an auxiliary binding function that ``picks'' out
 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
+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
+\isacommand{bind (res)}) or a list of atoms (for \isacommand{bind}). They can
 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:
 %
 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 @{text
 "fa_ty (C z\<^isub>1 \<dots> z\<^isub>n)"} will be the union @{text
 "fa(bc\<^isub>1) \<union> \<dots> \<union> fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding
-clause means. We only show the details for the mode \isacommand{bind\_set} (the other modes are similar).
+clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar).
 Suppose the binding clause @{text bc\<^isub>i} is of the form
 %
 \begin{center}
-\mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
+\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
 \end{center}
 \noindent
 in which the body-labels @{text "d"}$_{1..q}$ refer to types @{text ty}$_{1..q}$,
 and the binders @{text b}$_{1..p}$
 The task below is to specify what the premises of a binding clause are. As a
 special instance, we first treat the case where @{text "bc\<^isub>i"} is the
 empty binding clause of the form
 %
 \begin{center}
-\mbox{\isacommand{bind\_set} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+\mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
 \end{center}
 \noindent
 In this binding clause no atom is bound and we only have to $\alpha$-relate the bodies. For this
 we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
 We will use the unfolded version in the examples below.
 Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form
 %
 \begin{equation}\label{nonempty}
-\mbox{\isacommand{bind\_set} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
+\mbox{\isacommand{bind (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}.}
 \end{equation}
 \noindent
 In this case we define a premise @{text P} using the relation
 $\approx_{\,\textit{set}}$ given in Section~\ref{sec:binders} (similarly
 covers cases of binders depending on other binders, which just do not make
 sense for our $\alpha$-equated terms. Third, it allows empty types that have no
 meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's
 binding clauses. In Ott you specify binding clauses with a single body; we
 allow more than one. We have to do this, because this makes a difference
-for our notion of $\alpha$-equivalence in case of \isacommand{bind\_set} and
+for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and
-\isacommand{bind\_res}. Consider the examples
+\isacommand{bind (res)}. Consider the examples
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
 @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
-\isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t s"}\\
+\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
 @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
-\isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "t"},
+\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"},
-\isacommand{bind\_set} @{text "xs"} \isacommand{in} @{text "s"}\\
+\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
 \end{tabular}
 \end{center}
 \noindent
 In the first term-constructor we have a single
 it defines an equivalence relation. A complete
 reasoning infrastructure is well beyond the purposes of his language.
 In a slightly different domain (programming with dependent types), the
 paper \cite{Altenkirch10} presents a calculus with a notion of
-$\alpha$-equivalence related to our binding mode \isacommand{bind\_res}.
+$\alpha$-equivalence related to our binding mode \isacommand{bind (res)}.
 The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it
 has a more operational flavour and calculates a partial (renaming) map.
 In this way, the definition can deal with vacuous binders. However, to our
 best knowledge, no concrete mathematical result concerning this
 definition of $\alpha$-equivalence has been proved.
 general binders, that is term-constructors having multiple bound
 variables. For this extension we introduced new definitions of
 $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
 To specify general binders we used the specifications from Ott, but extended them
 in some places and restricted
-them in others so that they make sense in the context of $\alpha$-equated terms.
+them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not
+exist in Ott.
 We have tried out the extension with terms from Core-Haskell, type-schemes
 and the lambda-calculus, and our code
 will eventually become part of the next Isabelle distribution.\footnote{For the moment
 it can be downloaded from the Mercurial repository linked at
 \href{http://isabelle.in.tum.de/nominal/download}

changeset 2488	1c18f2cf3923
parent 2471	894599a50af3
child 2502	074304d56eb2