--- a/LMCS-Paper/Paper.thy Tue Sep 13 16:14:32 2011 +0200
+++ b/LMCS-Paper/Paper.thy Tue Sep 13 19:48:47 2011 +0200
@@ -685,7 +685,8 @@
Note that the relation is
dependent on a free-atom function @{text "fa"} and a relation @{text
"R"}. The reason for this extra generality is that we will use
- $\approx_{\,\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In
+ $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ for both ``raw'' terms and
+ alpha-equated terms. In
the latter case, @{text R} will be replaced by equality @{text "="} and we
will prove that @{text "fa"} is equal to @{text "supp"}.
@@ -770,7 +771,7 @@
\noindent
Note that in these relation we replaced the free-atom function @{text "fa"}
with @{term "supp"} and the relation @{text R} with equality. We can show
- the following properties:
+ the following two properties:
\begin{lem}\label{alphaeq}
The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$,
@@ -786,11 +787,13 @@
and @{text "\<pi>\<^isub>2"}, and for the proof obligation use @{text
"\<pi>\<^isub>1 + \<pi>\<^isub>2"}. Equivariance means @{term "alpha_set_ex (\<pi> \<bullet> as,
\<pi> \<bullet> x) equal supp (\<pi> \<bullet> bs, \<pi> \<bullet> y)"} holds provided \mbox{@{term
- "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. To show this, we need to
- unfold the definitions and `pull out' the permutations, which is possible
- since all operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"},
- are equivariant (see \cite{HuffmanUrban10}). Finally we apply the
- permutation operation on booleans.
+ "alpha_set_ex (as, x) equal supp(bs, y)"}} holds. From the assumption we
+ have a permutation @{text "\<pi>'"} and for the proof obligation use @{text "\<pi> \<bullet>
+ \<pi>'"}. To show then equivariance, we need to `pull out' the permutations,
+ which is possible since all operators, namely as @{text "#\<^sup>*, -, =, \<bullet>,
+ set"} and @{text "supp"}, are equivariant (see
+ \cite{HuffmanUrban10}). Finally, we apply the permutation operation on
+ booleans.
\end{proof}
\noindent
@@ -861,9 +864,11 @@
\end{lem}
\begin{proof}
- This lemma is straightforward using \eqref{abseqiff} and observing that
- the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
- We therefore can use as permutation the swapping @{term "(a \<rightleftharpoons> b)"}.
+ If @{term "a = b"} the lemma is immediate, since @{term "(a \<rightleftharpoons> b) = 0"}.
+ Also in the other case, it is straightforward using \eqref{abseqiff} and
+ observing that the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) =
+ (supp x - as)"}. We therefore can use as permutation the swapping @{term
+ "(a \<rightleftharpoons> b)"}.
\end{proof}
\noindent
@@ -908,7 +913,7 @@
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
the first equation of Theorem~\ref{suppabs}.
- Recall the definition of support \eqref{suppdef}, and note the difference between
+ Recall the definition of support in \eqref{suppdef}, and note the difference between
the support of a ``raw'' pair and an abstraction
\[
@@ -917,7 +922,7 @@
\]\smallskip
\noindent
- While the permutation operations behave in both cases the same (the permutation
+ While the permutation operations behave in both cases the same (a permutation
is just moved to the arguments), the notion of equality is different for pairs and
abstractions. Therefore we have different supports.
@@ -1282,6 +1287,9 @@
@{text "\<pi> \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (\<pi> \<bullet> z\<^isub>1) \<dots> (\<pi> \<bullet> z\<^isub>n)"}
\end{equation}\smallskip
+ \noindent
+ We need this operation later when we define the notion of alpha-equivalence.
+
The first non-trivial step we have to perform is the generation of
\emph{free-atom functions} from the specifications.\footnote{Admittedly, the
details of our definitions will be somewhat involved. However they are still
@@ -1306,13 +1314,13 @@
\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.
+ bound, as we saw in the example with ``plain'' @{text Let}s. We need
+ therefore functions that calculate those free atoms in deep binders.
- While the idea behind these free-atom functions is clear (they just
+ While the idea behind these free-atom functions is simple (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
+ a ``raw'' 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
@@ -1377,7 +1385,9 @@
\noindent
where we use the auxiliary binding functions from \eqref{bnaux} for shallow
binders (that means when @{text "ty"}$_i$ is of type @{text "atom"}, @{text "atom set"} or
- @{text "atom list"}). The set @{text "B'"} in \eqref{fadef} collects all free atoms in
+ @{text "atom list"}).
+
+ The set @{text "B'"} in \eqref{fadef} collects all free atoms in
non-recursive deep binders. Let us assume these binders in the binding
clause @{text "bc\<^isub>i"} are
@@ -1578,7 +1588,7 @@
involving multiple binders. As above, we first build the tuples @{text "D"} and
@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
compound alpha-relation @{text "R"} (shown in \eqref{rempty}).
- For $\approx_{\,\textit{set}}^{R, fa}$ we also need
+ For $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ we also need
a compound free-atom function for the bodies defined as
\[
@@ -1666,7 +1676,7 @@
for the existentially quantified permutation).
Again let us take a look at a concrete example for these definitions. For
- teh specification given in \eqref{letrecs}
+ the specification given in \eqref{letrecs}
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$ with the following clauses:
@@ -1704,9 +1714,10 @@
The underlying reason is that the terms inside an assignment are not meant
to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"},
because there all components of an assignment are ``under'' the binder.
- Note also that in case of more than one body (e.g.~@{text "Let_rec"}-case)
- we need to parametrise the relation $\approx_{\textit{list}}$ with compound
- equivalence relations and compund free-atom functions.
+ Note also that in case of more than one body (e.g.~in the @{text "Let_rec"}-case)
+ we need to parametrise the relation $\approx_{\textit{list}}$ with a compound
+ equivalence relation and a compound free-atom function. This is because the
+ corresponding binding cluase specifies a binder with two bodies.
*}
section {* Establishing the Reasoning Infrastructure *}
@@ -1730,11 +1741,12 @@
\end{lem}
\begin{proof}
- The function package of Isabelle/HOL allows us to prove the first part is by
- mutual induction over the definitions of the functions (we know that they
- are terminating functions, from which an induction principle can be
- derived). The second is by a straightforward induction over the rules of
- @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using the first part.
+ The function package of Isabelle/HOL \cite{Krauss09} allows us to prove the
+ first part is by mutual induction over the definitions of the functions.\footnote{We
+ know that they are terminating functions. From this an induction principle
+ is derived by the function package.} The second is by a straightforward
+ induction over the rules of @{text "\<approx>ty"}$_{1..n}$ and @{text "\<approx>bn"}$_{1..m}$ using
+ the first part.
\end{proof}
\noindent
@@ -1758,7 +1770,7 @@
We can feed the last lemma into our quotient package and obtain new types
@{text "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types
@{text "ty"}$_{1..n}$. We also obtain definitions for the term-constructors
- @{text "C"}$^\alpha_{1..k}$ from the raw term-constructors @{text
+ @{text "C"}$^\alpha_{1..k}$ from the ``raw'' term-constructors @{text
"C"}$_{1..k}$, and similar definitions for the free-atom functions @{text
"fa_ty"}$^\alpha_{1..n}$ and @{text "fa_bn"}$^\alpha_{1..m}$ as well as the
binding functions @{text "bn"}$^\alpha_{1..m}$. However, these definitions
@@ -1784,9 +1796,9 @@
\end{equation}\smallskip
\noindent
- holds for the corresponding raw term-constructors.
+ holds for the corresponding ``raw'' term-constructors.
In order to deduce \eqref{distinctalpha} from \eqref{distinctraw}, our quotient
- package needs to know that the raw term-constructors @{text "C"} and @{text "D"}
+ package needs to know that the ``raw'' term-constructors @{text "C"} and @{text "D"}
are \emph{respectful} w.r.t.~the alpha-equivalence relations (see \cite{Homeier05}).
Given, for example, @{text "C"} is of type @{text "ty"} with argument types
@{text "ty"}$_{1..r}$, respectfulness amounts to showing that
@@ -1798,7 +1810,7 @@
\noindent
holds under the assumptions \mbox{@{text
"x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"}
- and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and
+ and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C}, and
@{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments
(similarly for @{text "D"}). For this we have to show
by induction over the definitions of alpha-equivalences the following
@@ -1815,19 +1827,18 @@
\noindent
whereby @{text "ty\<^isub>l"} is the type over which @{text "bn\<^isub>j"}
- is defined. These implications can be established by induction on @{text
- "\<approx>ty"}$_{1..n}$. Whereas the first, second and last implication are true by
+ is defined. Whereas the first, second and last implication are true by
how we stated our definitions, the third \emph{only} holds because of our
restriction imposed on the form of the binding functions---namely \emph{not}
- returning any bound atoms. In Ott, in contrast, the user may define @{text
+ to return any bound atoms. In Ott, in contrast, the user may define @{text
"bn"}$_{1..m}$ so that they return bound atoms and in this case the third
- implication is \emph{not} true. A result is that the lifting of the
+ implication is \emph{not} true. A result is that in general the lifting of the
corresponding binding functions in Ott to alpha-equated terms is impossible.
- Having established respectfulness for the raw term-constructors, the
+ Having established respectfulness for the ``raw'' term-constructors, the
quotient package is able to automatically deduce \eqref{distinctalpha} from
\eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can
- also lift properties that characterise when two raw terms of the form
+ also lift properties that characterise when two ``raw'' terms of the form
\[
\mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>r \<approx>ty C x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}}
@@ -1843,7 +1854,9 @@
\noindent
We call these conditions as \emph{quasi-injectivity}. They correspond to
- the premises in our alpha-equiva\-lence relations.
+ the premises in our alpha-equiva\-lence relations, with the exception that
+ in case of binders the relations $\approx_{\textit{set}}^{\textit{R}, \textit{fa}}$
+ are replaced by $\approx_{\textit{set}}^{=, \textit{fa}}$.
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
@@ -1864,13 +1877,13 @@
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 cases lemmas and a structural
+ Finally we can add to our infrastructure cases lemmas and a (mutual)
induction principle for the types @{text "ty\<AL>"}$_{1..n}$. The cases
lemmas allow the user to deduce a property @{text "P"} by exhaustively
- analysing all cases how the elements in a type @{text "ty\<AL>"}$_i$ can
- be constructed (that means one case for each of term-constructors @{text "C\<AL>"}$_{1..m}$
- of type @{text "ty\<AL>"}$_i\,$). These are lifted versions of the cases
- lemma over the raw type @{text "ty"}$_i$ and schematically look as
+ analysing all cases how an element in a type @{text "ty\<AL>"}$_i$ can
+ be constructed (that means one case for each of term-constructors
+ of type @{text "ty\<AL>"}$_i\,$). The lifted cases
+ lemma for the type @{text "ty\<AL>"}$_i\,$ looks as
follows
\[
@@ -1884,8 +1897,9 @@
\noindent
where @{text "y"} is a variable of type @{text "ty"}$_i$ and @{text "P"} is the
- property that is established by the case analysis. Similarly, we have an induction
- principle for the types @{text "ty\<AL>"}$_{1..n}$, which is
+ property that is established by the case analysis. Similarly, we have a (mutual)
+ induction principle for the types @{text "ty\<AL>"}$_{1..n}$, which is of the
+ form
\[
\infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
@@ -1899,17 +1913,20 @@
\noindent
whereby the @{text P}$_{1..n}$ are the properties established by induction
and the @{text y}$_{1..n}$ are of type @{text "ty\<AL>"}$_{1..n}$.
- This induction principle has for all term constructors @{text "C"}$^\alpha$
+ This induction principle has for the term constructors @{text "C"}$^\alpha_1$
a premise of the form
\begin{equation}\label{weakprem}
- \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>r. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"}}
+ \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}}
\end{equation}\smallskip
\noindent
- in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..r}$ are
- the recursive arguments of the term constructor. In case of the lambda-calculus,
- the cases lemma and the induction principle boil down to the following:
+ in which the @{text "x"}$_{i..j}$ @{text "\<subseteq>"} @{text "x"}$_{1..k}$ are
+ the recursive arguments of this term constructor (similarly for the other
+ term-constructors). In case of the lambda-calculus (with constructors
+ @{text "Var\<^sup>\<alpha>"}, @{text "App\<^sup>\<alpha>"} and @{text "Lam\<^sup>\<alpha>"}),
+ the cases lemmas and the induction principle boil down to the following
+ two inference rules:
\[\mbox{
\begin{tabular}{c@ {\hspace{10mm}}c}
@@ -1929,6 +1946,12 @@
\end{tabular}}
\]\smallskip
+ \noindent
+ We will show in the next section that these inference rules are not very
+ convenient for the user to establish properties about lambda-terms, but
+ they are crucial for completing our reasoning infrastructure for the
+ types @{text "ty\<AL>"}$_{1..n}$.
+
By working now completely on the alpha-equated level, we
can first show that the free-atom functions and binding functions are
equivariant, namely
@@ -1945,7 +1968,7 @@
\noindent
These properties can be established using the induction principle for the
types @{text "ty\<AL>"}$_{1..n}$. Having these
- equivariant properties established, we can show that the support of
+ equivariant properties at our disposal, we can show that the support of
term-constructors @{text "C\<^sup>\<alpha>"} is included in the support of its
arguments, that means
@@ -1956,9 +1979,10 @@
\noindent
holds. This allows us to prove by induction that every @{text x} of type
@{text "ty\<AL>"}$_{1..n}$ is finitely supported. This can be again shown by
- induction over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the
+ the induction principle for @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the
support of elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text
- "fa_ty\<AL>"}$_{1..n}$. This fact is important in the nominal setting, but
+ "fa_ty\<AL>"}$_{1..n}$. This fact is important in the nominal setting
+ where the general theory is formulated in terms of @{text "supp"} and @{text "#"}, but
also provides evidence that our notions of free-atoms and alpha-equivalence
are sensible.
@@ -1977,81 +2001,10 @@
\noindent
To sum up this section, we can establish 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
+ 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
- %specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
-
- %\begin{figure}[t!]
- %\begin{boxedminipage}{\linewidth}
- %\small
- %\begin{tabular}{l}
- %\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
- %\isacommand{nominal\_datatype}~@{text "tkind ="}\\
- %\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
- %\isacommand{and}~@{text "ckind ="}\\
- %\phantom{$|$}~@{text "CKSim ty ty"}\\
- %\isacommand{and}~@{text "ty ="}\\
- %\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
- %$|$~@{text "TFun string ty_list"}~%
- %$|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
- %$|$~@{text "TArr ckind ty"}\\
- %\isacommand{and}~@{text "ty_lst ="}\\
- %\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
- %\isacommand{and}~@{text "cty ="}\\
- %\phantom{$|$}~@{text "CVar cvar"}~%
- %$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
- %$|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
- %$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
- %$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
- %$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
- %\isacommand{and}~@{text "co_lst ="}\\
- %\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
- %\isacommand{and}~@{text "trm ="}\\
- %\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
- %$|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
- %$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
- %$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
- %$|$~@{text "Lam v::var ty t::trm"} \isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
- %$|$~@{text "Let x::var ty trm t::trm"} \isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
- %$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
- %\isacommand{and}~@{text "assoc_lst ="}\\
- %\phantom{$|$}~@{text ANil}~%
- %$|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
- %\isacommand{and}~@{text "pat ="}\\
- %\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
- %\isacommand{and}~@{text "vt_lst ="}\\
- %\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
- %\isacommand{and}~@{text "tvtk_lst ="}\\
- %\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
- %\isacommand{and}~@{text "tvck_lst ="}\\
- %\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
- %\isacommand{binder}\\
- %@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
- %@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
- %@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
- %@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
- %\isacommand{where}\\
- %\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
- %$|$~@{text "bv1 VTNil = []"}\\
- %$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
- %$|$~@{text "bv2 TVTKNil = []"}\\
- %$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
- %$|$~@{text "bv3 TVCKNil = []"}\\
- %$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
- %\end{tabular}
- %\end{boxedminipage}
- %\caption{The nominal datatype declaration for Core-Haskell. For the moment we
- %do not support nested types; therefore we explicitly have to unfold the
- %lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
- %in a future version of Nominal Isabelle. Apart from that, the
- %declaration follows closely the original in Figure~\ref{corehas}. The
- %point of our work is that having made such a declaration in Nominal Isabelle,
- %one obtains automatically a reasoning infrastructure for Core-Haskell.
- %\label{nominalcorehas}}
- %\end{figure}
*}
@@ -2349,15 +2302,14 @@
numbers, one referring to the place where a variable is bound, and the other
to which variable is bound. The reasoning infrastructure for both
representations of bindings comes for free in theorem provers like
- Isabelle/HOL or Coq, since the corresponding term-calculi can be implemented
+ Isabelle/HOL and Coq, since the corresponding term-calculi can be implemented
as ``normal'' datatypes. However, in both approaches it seems difficult to
achieve our fine-grained control over the ``semantics'' of bindings
(i.e.~whether the order of binders should matter, or vacuous binders should
be taken into account). To do so, one would require additional predicates
that filter out unwanted terms. Our guess is that such predicates result in
- rather intricate formal reasoning. We are not aware of any non-trivial
- formalisation that uses Chargu\'eraud's idea.
-
+ rather intricate formal reasoning. We are not aware of any formalisation of
+ a non-trivial language that uses Chargu\'eraud's idea.
Another technique for representing binding is higher-order abstract syntax
(HOAS), which for example is implemented in the Twelf system. This
@@ -2389,7 +2341,7 @@
Sewell et al \cite{ott-jfp} and the C$\alpha$ml language by Pottier
\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 Ott can also generate theorem prover code using a raw
+ 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 and free variables for terms that can be
@@ -2398,7 +2350,7 @@
result concerning this notion of alpha-equivalence and free variables. We
have proved that our definitions lead to alpha-equated terms, whose support
is as expected (that means bound names are removed from the support). We
- also showed that our specifications lift from a raw type to a type of
+ also showed that our specifications lift from ``raw'' types to types of
alpha-equivalence classes. For this we had to establish (automatically) that every
term-constructor and function is repectful w.r.t.~alpha-equivalence.
@@ -2458,7 +2410,64 @@
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. ???
+ example Core-Haskell (see Figure~\ref{nominalcorehas}).
+
+ \begin{figure}[p!]
+ \begin{boxedminipage}{\linewidth}
+ \small
+ \begin{tabular}{l}
+ \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
+ \isacommand{nominal\_datatype}~@{text "tkind ="}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\
+ \isacommand{and}~@{text "ckind ="}~@{text "CKSim ty ty"}\\
+ \isacommand{and}~@{text "ty ="}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+ $|$~@{text "TFun string ty_list"}~%
+ $|$~@{text "TAll tv::tvar tkind ty::ty"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+ $|$~@{text "TArr ckind ty"}\\
+ \isacommand{and}~@{text "ty_lst ="}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+ \isacommand{and}~@{text "cty ="}~@{text "CVar cvar"}~%
+ $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+ $|$~@{text "CAll cv::cvar ckind cty::cty"}\hspace{3mm}\isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+ $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+ $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+ $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+ \isacommand{and}~@{text "co_lst ="}~@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+ \isacommand{and}~@{text "trm ="}~@{text "Var var"}~$|$~@{text "K string"}\\
+ $|$~@{text "LAM_ty tv::tvar tkind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "LAM_cty cv::cvar ckind t::trm"}\hspace{3mm}\isacommand{binds}~@{text "cv"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+ $|$~@{text "Lam v::var ty t::trm"}\hspace{3mm}\isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\
+ $|$~@{text "Let x::var ty trm t::trm"}\hspace{3mm}\isacommand{binds}~@{text x}~\isacommand{in}~@{text t}\\
+ $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+ \isacommand{and}~@{text "assoc_lst ="}~@{text ANil}~%
+ $|$~@{text "ACons p::pat t::trm assoc_lst"}\hspace{3mm}\isacommand{binds}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+ \isacommand{and}~@{text "pat ="}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+ \isacommand{and}~@{text "vt_lst ="}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+ \isacommand{and}~@{text "tvtk_lst ="}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+ \isacommand{and}~@{text "tvck_lst ="}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+ \isacommand{binder}\\
+ @{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}\\
+ @{text "bv\<^isub>1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+ @{text "bv\<^isub>2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+ @{text "bv\<^isub>3 :: tvck_lst \<Rightarrow> atom list"}\\
+ \isacommand{where}\\
+ \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv\<^isub>3 tvts) @ (bv\<^isub>2 tvcs) @ (bv\<^isub>1 vs)"}\\
+ $|$~@{text "bv\<^isub>1 VTNil = []"}\\
+ $|$~@{text "bv\<^isub>1 (VTCons x ty tl) = (atom x)::(bv\<^isub>1 tl)"}\\
+ $|$~@{text "bv\<^isub>2 TVTKNil = []"}\\
+ $|$~@{text "bv\<^isub>2 (TVTKCons a ty tl) = (atom a)::(bv\<^isub>2 tl)"}\\
+ $|$~@{text "bv\<^isub>3 TVCKNil = []"}\\
+ $|$~@{text "bv\<^isub>3 (TVCKCons c cty tl) = (atom c)::(bv\<^isub>3 tl)"}\\
+ \end{tabular}
+ \end{boxedminipage}
+ \caption{The nominal datatype declaration for Core-Haskell. For the moment we
+ do not support nested types; therefore we explicitly have to unfold the
+ lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the
+ declaration follows closely the original in Figure~\ref{corehas}. The
+ point of our work is that having made such a declaration in Nominal Isabelle,
+ one obtains automatically a reasoning infrastructure for Core-Haskell.
+ \label{nominalcorehas}}
+ \end{figure}
+
Pottier presents a programming language, called C$\alpha$ml, for
representing terms with general binders inside OCaml \cite{Pottier06}. This
@@ -2506,12 +2515,12 @@
{http://isabelle.in.tum.de/nominal/download}.}
We have left out a discussion about how functions can be defined over
- alpha-equated terms involving general binders. In earlier versions of Nominal
- Isabelle this turned out to be a thorny issue. We
- hope to do better this time by using the function package that has recently
+ alpha-equated terms involving general binders. In earlier versions of
+ Nominal Isabelle this turned out to be a thorny issue. We hope to do better
+ this time by using the function package \cite{Krauss09} that has recently
been implemented in Isabelle/HOL and also by restricting function
- definitions to equivariant functions (for them we can
- provide more automation).
+ definitions to equivariant functions (for them we can provide more
+ automation).
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