nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:2ccf3086142b
+:b5cb3183409e
 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 "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-in which the generic type @{text "\<beta>"} stands for the type of the object
+where the generic type @{text "\<beta>"} stands for the type of the object
 over 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 by induction over the type-hierarchy \cite{HuffmanUrban10};
+operation is defined over the type-hierarchy \cite{HuffmanUrban10};
 for example permutations acting on products, lists, sets, functions and booleans is
 given by:
 %
 \begin{equation}\label{permute}
 \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last
 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders
 @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 Most properties given in this section are described in detail in \cite{HuffmanUrban10}
-and of course all are formalised in Isabelle/HOL. In the next sections we will make
+and all are formalised in Isabelle/HOL. In the next sections we will make
 extensive use of these properties in order to define $\alpha$-equivalence in
 the presence of multiple binders.
 *}
 \end{equation}
 \noindent
 (similarly for $\approx_{\,\textit{abs\_res}}$
 and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence
-relations and equivariant.
+relations. %% and equivariant.
 \begin{lemma}\label{alphaeq}
 The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
-and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
+and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if
-"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
+%@{term "abs_set (as, x) (bs, y)"} then also
-bs, p \<bullet> y)"} (similarly for the other two relations).
+%@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
 \end{lemma}
 \begin{proof}
 Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
 a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
 %\cite{Berghofer99}.
 The labels
 annotated on the types are optional. Their purpose is to be used in the
 (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}
+\begin{tabular}{@ {}l@ {}}
-\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+\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);
 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). As indicated, the labels in the ``\isacommand{in}-part'' of a binding
 tuple patterns might be specified as:
 %
 \begin{equation}\label{letpat}
 \mbox{\small%
 \begin{tabular}{l}
-\isacommand{nominal\_datatype} @{text trm} =\\
+\isacommand{nominal\_datatype} @{text trm} $=$\\
 \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
 \hspace{5mm}$\mid$~@{term "App trm trm"}\\
 \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"}
 \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"}
 \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
-\isacommand{and} @{text pat} =\\
+\isacommand{and} @{text pat} $=$
-\hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
+@{text PNil}
-\hspace{5mm}$\mid$~@{text "PVar name"}\\
+$\mid$~@{text "PVar name"}
-\hspace{5mm}$\mid$~@{text "PTup pat pat"}\\
+$\mid$~@{text "PTup pat pat"}\\
 \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
 \isacommand{where}~@{text "bn(PNil) = []"}\\
 \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
 \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\
 \end{tabular}}
 specification:
 %
 \begin{equation}\label{letrecs}
 \mbox{\small%
 \begin{tabular}{@ {}l@ {}}
-\isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\
+\isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
 \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
 \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
 \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
-\isacommand{and} @{text "ass"} =\\
+\isacommand{and} @{text "assn"} $=$
-\hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+@{text "ANil"}
-\hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
+$\mid$~@{text "ACons name trm assn"}\\
 \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
 \isacommand{where}~@{text "bn(ANil) = []"}\\
 \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
 \end{tabular}}
 \end{equation}
 The first non-trivial step we have to perform is the generation of
 free-atom functions from the specification. For the
 \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
 %
-\begin{equation}\label{fvars}
+%\begin{equation}\label{fvars}
-@{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
+@{text "fa_ty\<^isub>"}$_{1..n}$
-\end{equation}
+%\end{equation}
+%
-\noindent
+%\noindent
 by recursion.
 We define these functions together with auxiliary free-atom functions for
 the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$
 we define
 %
-\begin{center}
+%\begin{center}
-@{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
+@{text "fa_bn\<^isub>"}$_{1..m}$.
-\end{center}
+%\end{center}
+%
-\noindent
+%\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 free atoms in a deep binder.
 While the idea behind these free-atom functions is clear (they just
 \end{center}
 \noindent
 where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the
 specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function
-we are defining by recursion
+we are defining by recursion;
-(see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+%(see \eqref{fvars});
+otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
 In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
 for atom types to which shallow binders may refer
 %
 %\begin{center}
 @{text "bn_atom_list as \<equiv> atoms (set as)"}
 \end{center}
 \noindent
 Like the function @{text atom}, the function @{text "atoms"} coerces
-a set of atoms to a set of the generic atom type. It is defined as
+a set of atoms to a set of the generic atom type.
-@{text "atoms as \<equiv> {atom a | a \<in> as}"}.
+%It is defined as  @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
 The set @{text B} is then formally defined as
 %
 \begin{center}
 @{text "B \<equiv> bn_ty\<^isub>1 b\<^isub>1 \<union> ... \<union> bn_ty\<^isub>p b\<^isub>p"}
 \end{center}
 "ANil"} and @{text "ACons"}. Since there is a binding function defined for
 assignments, we have three free-atom functions, namely @{text
 "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
 "fa\<^bsub>bn\<^esub>"} as follows:
 %
-\begin{center}
+\begin{center}\small
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
 @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
 @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
 Next we define the $\alpha$-equivalence relations for the raw types @{text
 "ty"}$_{1..n}$ from the specification. We write them as
 %
 %\begin{center}
-@{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}.
+@{text "\<approx>ty"}$_{1..n}$.
 %\end{center}
 %
 %\noindent
 Like with the free-atom functions, we also need to
 define auxiliary $\alpha$-equivalence relations
 %
 %\begin{center}
-@{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
+@{text "\<approx>bn\<^isub>"}$_{1..m}$
 %\end{center}
 %
 %\noindent
 for the binding functions @{text "bn"}$_{1..m}$,
 To simplify our definitions we will use the following abbreviations for
 \emph{compound equivalence relations} and \emph{compound free-atom functions} acting on tuples
 %
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-@{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
+@{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
-@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
+@{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
-@{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\
+@{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\
 \end{tabular}
 \end{center}
 The $\alpha$-equivalence relations are defined as inductive predicates
 Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$ with the following clauses:
-\begin{center}
+\begin{center}\small
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
 {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
 \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
 {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
 \end{tabular}
 \end{center}
-\begin{center}
+\begin{center}\small
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
 \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
 {@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
 \end{tabular}
 \end{center}
-\begin{center}
+\begin{center}\small
 \begin{tabular}{@ {}c @ {}}
 \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
 \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
 {@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
 \end{tabular}
 equivalence relations.
 \begin{lemma}\label{equiv}
 Given the raw types @{text "ty"}$_{1..n}$ and binding functions
 @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and
-@{text "\<approx>bn"}$_{1..m}$ are equivalence relations and equivariant.
+@{text "\<approx>bn"}$_{1..m}$ are equivalence relations.%% and equivariant.
 \end{lemma}
 \begin{proof}
 The proof is by mutual induction over the definitions. The non-trivial
 cases involve premises built up by $\approx_{\textit{set}}$,
 Next we can lift the permutation
 operations defined in \eqref{ceqvt}. In order to make this
 lifting to go through, we have to show that the permutation operations are respectful.
 This amounts to showing that the
-$\alpha$-equivalence relations are equivariant, which we already established
+$\alpha$-equivalence relations are equivariant \cite{HuffmanUrban10}.
-in Lemma~\ref{equiv}. As a result we can add the equations
+%, which we already established
+%in Lemma~\ref{equiv}.
+As a result we can add the equations
 %
 \begin{equation}\label{calphaeqvt}
 @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
 \end{equation}
 @{text "fa_bn\<AL>"}$_{1..m}$ as well as of the binding functions @{text
 "bn\<AL>"}$_{1..m}$ and the size functions @{text "size_ty\<AL>"}$_{1..n}$.
 The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
 by the datatype package of Isabelle/HOL.
-Finally we can add to our infrastructure a structural induction principle
+Finally we can add to our infrastructure a cases lemma (explained in the next section)
-for the types @{text "ty\<AL>"}$_{i..n}$ whose
+and a structural induction principle
-conclusion of the form
+for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
+of the form
 %
 \begin{equation}\label{weakinduct}
 \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
 \end{equation}
 \noindent
 To sum up this section, we can established automatically a reasoning infrastructure
 for the types @{text "ty\<AL>"}$_{1..n}$
 by first lifting definitions from the raw level to the quotient level and
 then by establishing facts about these lifted definitions. All necessary proofs
-are generated automatically by custom ML-code. This code can deal with
+are generated automatically by custom ML-code.
-specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
+%This code can deal with
+%specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
 %\begin{figure}[t!]
 %\begin{boxedminipage}{\linewidth}
 %\small
 %\begin{tabular}{l}
 example in the second part of this challenge, @{text "Let"}s involve
 patterns that bind multiple variables at once. In such situations, HOAS
 representations have to resort to the iterated-single-binders-approach with
 all the unwanted consequences when reasoning about the resulting terms.
-Two formalisations involving general binders have been
+%Two formalisations involving general binders have been
-performed in older
+%performed in older
-versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
+%versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
-\cite{BengtsonParow09,UrbanNipkow09}).  Both
+%\cite{BengtsonParow09,UrbanNipkow09}).  Both
-use the approach based on iterated single binders. Our experience with
+%use the approach based on iterated single binders. Our experience with
-the latter formalisation has been disappointing. The major pain arose from
+%the latter formalisation has been disappointing. The major pain arose from
-the need to ``unbind'' variables. This can be done in one step with our
+%the need to ``unbind'' variables. This can be done in one step with our
-general binders described in this paper, but needs a cumbersome
+%general binders described in this paper, but needs a cumbersome
-iteration with single binders. The resulting formal reasoning turned out to
+%iteration with single binders. The resulting formal reasoning turned out to
-be rather unpleasant. The hope is that the extension presented in this paper
+%be rather unpleasant. The hope is that the extension presented in this paper
-is a substantial improvement.
+%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
 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
-\isacommand{bind (res)}. Consider the examples
+\isacommand{bind (res)}.
-\begin{center}
+%Consider the examples
-\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
+%
-@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &
+%\begin{center}
-\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
+%\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
-@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
+%@{text "Foo\<^isub>1 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 s"}\\
-\isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
+%@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &
-\end{tabular}
+%    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"},
-\end{center}
+%    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
+%\end{tabular}
-\noindent
+%\end{center}
-In the first term-constructor we have a single
+%
-body that happens to be ``spread'' over two arguments; in the second term-constructor we have
+%\noindent
-two independent bodies in which the same variables are bound. As a result we
+%In the first term-constructor we have a single
-have
+%body that happens to be ``spread'' over two arguments; in the second term-constructor we have
+%two independent bodies in which the same variables are bound. As a result we
-\begin{center}
+%have
-\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+%
-@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
+%\begin{center}
-@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
+%\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
-@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
+%@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ &
-@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+%@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
-\end{tabular}
+%@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ &
-\end{center}
+%@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+%\end{tabular}
-\noindent
+%\end{center}
-and therefore need the extra generality to be able to distinguish between
-both specifications.
+\noindent
+%and therefore need the extra generality to be able to distinguish between
+%both specifications.
 Because of how we set up our definitions, we also had to impose some restrictions
 (like a single binding function for a deep binder) that are not present in Ott. Our
 expectation is that we can still cover many interesting term-calculi from
 programming language research, for example Core-Haskell.
 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. We also introduced two binding modes (set and res) that do not
+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
+and a dozen of other calculi from programming language research. The 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}
 {http://isabelle.in.tum.de/nominal/download}.}
 hope to do better this time by using the function package that has recently
 been implemented in Isabelle/HOL and also by restricting function
 definitions to equivariant functions (for such functions it is possible to
 provide more automation).
-There are some restrictions we imposed in this paper that we would like to lift in
+%There are some restrictions we imposed in this paper that we would like to lift in
-future work. One is the exclusion of nested datatype definitions. Nested
+%future work. One is the exclusion of nested datatype definitions. Nested
-datatype definitions allow one to specify, for instance, the function kinds
+%datatype definitions allow one to specify, for instance, the function kinds
-in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
+%in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
-version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
+%version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
-achieve this, we need a slightly more clever implementation than we have at the moment.
+%achieve this, we need a slightly more clever implementation than we have at the moment.
-A more interesting line of investigation is whether we can go beyond the
+%A more interesting line of investigation is whether we can go beyond the
-simple-minded form of binding functions that we adopted from Ott. At the moment, binding
+%simple-minded form of binding functions that we adopted from Ott. At the moment, binding
-functions can only return the empty set, a singleton atom set or unions
+%functions can only return the empty set, a singleton atom set or unions
-of atom sets (similarly for lists). It remains to be seen whether
+%of atom sets (similarly for lists). It remains to be seen whether
-properties like
+%properties like
-%
+%%
-\begin{center}
+%\begin{center}
-@{text "fa_ty x  =  bn x \<union> fa_bn x"}.
+%@{text "fa_ty x  =  bn x \<union> fa_bn x"}.
-\end{center}
+%\end{center}
+%
-\noindent
+%\noindent
-allow us to support more interesting binding functions.
+%allow us to support more interesting binding functions.
+%
-We have also not yet played with other binding modes. For example we can
+%We have also not yet played with other binding modes. For example we can
-imagine that there is need for a binding mode
+%imagine that there is need for a binding mode
-where instead of lists, we abstract lists of distinct elements.
+%where instead of lists, we abstract lists of distinct elements.
-Once we feel confident about such binding modes, our implementation
+%Once we feel confident about such binding modes, our implementation
-can be easily extended to accommodate them.
+%can be easily extended to accommodate them.
 \medskip
 \noindent
 {\bf Acknowledgements:} %We are very grateful to Andrew Pitts for
 %many discussions about Nominal Isabelle.

changeset 2512	b5cb3183409e
parent 2511	2ccf3086142b
child 2513	ae860c95bf9f