--- a/LMCS-Paper/Paper.thy Fri Apr 20 15:28:35 2012 +0200
+++ b/LMCS-Paper/Paper.thy Fri Apr 20 15:29:40 2012 +0200
@@ -129,10 +129,10 @@
address the following problem:
Given a type-scheme, say @{text S}, how does one get access to the bound type-variables
and the type-part of @{text S}? The unbinding relation gives an answer to this problem, though
- in general it will only provide some list of type-variables together with a type that are
+ in general it will only provide \emph{a} list of type-variables together with \emph{a} type that are
``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
- for alpha-equated type-schemes. With this
- definition in place we can formally define when a type is an instance of a type-scheme as follows:
+ for alpha-equated type-schemes. With the unbinding relation
+ in place, we can define when a type @{text T} is an instance of a type-scheme @{text S} as follows:
\[
@{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
@@ -144,15 +144,15 @@
@{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
The problem with this definition is that we cannot follow the usual proofs
that are by induction on the type-part of the type-scheme (since it is under
- an existential quantifier and only an alpha-variant). The representation of
+ an existential quantifier and only an alpha-variant). The implementation of
type-schemes using iterations of single binders
prevents us from directly ``unbinding'' the bound type-variables and the type-part.
- Clearly, some more dignified approach to formalising algorithm W is desirable.
+ Clearly, a more dignified approach for formalising algorithm W is desirable.
The purpose of this paper is to introduce general binders, which
allow us to represent type-schemes so that they can bind multiple variables at once
and as a result solve this problem more straightforwardly.
The need of iterating single binders is also one reason
- why Nominal Isabelle and similar theorem provers that only provide
+ why the existing Nominal Isabelle and similar theorem provers that only provide
mechanisms for binding single variables have so far not fared very well with
the more advanced tasks in the POPLmark challenge \cite{challenge05},
because also there one would like to bind multiple variables at once.
@@ -1290,7 +1290,7 @@
To sum up this section, we introduced nominal datatype
specifications, which are like standard datatype specifications in
- Isabelle/HOL extended with specifications for binding
+ Isabelle/HOL but extended with binding clauses and specifications for binding
functions. Each constructor argument in our specification can also
have an optional label. These labels are used in the binding clauses
of a constructor; there can be several binding clauses for each
@@ -1303,13 +1303,15 @@
can also occur in more than one binding clause, unless they are
recursive in which case they can only occur once. Each of the deep
binders can only have a single binding function. Binding functions
- are defined by recursion over a nominal datatype. They can only
+ are defined by recursion over a nominal datatype. They can
return the empty set, singleton atoms and unions of sets of atoms
(for binding modes \isacommand{binds (set)} and \isacommand{binds
(set+)}), and the empty list, singleton atoms and appended lists of
atoms (for mode \isacommand{bind}). However, they can only return
- atoms that are not mentioned in any binding clause. In order to
- simplify our definitions of free atoms and alpha-equivalence, we
+ atoms that are not mentioned in any binding clause.
+
+ In order to
+ simplify our definitions of free atoms and alpha-equivalence we define next, 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
@@ -1413,7 +1415,7 @@
"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{binds (set)} (the other modes are similar).
- Suppose the binding clause @{text bc\<^isub>i} is of the form
+ Suppose a binding clause @{text bc\<^isub>i} is of the form
\[
\mbox{\isacommand{binds (set)} @{text "b\<^isub>1\<dots>b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\<dots>d\<^isub>q"}}
@@ -1614,10 +1616,10 @@
term-constructor @{text C} is of type @{text ty} and has the binding clauses
@{term "bc"}$_{1..k}$, then the alpha-equivalence clause has the form
- \[
+ \begin{equation}\label{gform}
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>n \<approx>ty C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>n"}}
{@{text "prems(bc\<^isub>1) \<dots> prems(bc\<^isub>k)"}}}
- \]\smallskip
+ \end{equation}\smallskip
\noindent
The task below is to specify what the premises corresponding to a binding
@@ -1634,8 +1636,8 @@
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)"}
whereby the labels @{text "d"}$_{1..q}$ refer to some of the arguments @{text
- "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of @{text
- "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such
+ "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of the @{text
+ "z\<PRIME>"}$_{1..n}$ in \eqref{gform}. In order to relate two such
tuples we define the compound alpha-equivalence relation @{text "R"} as
follows
@@ -1648,7 +1650,7 @@
labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a
recursive argument of @{text C} and have type @{text "ty\<^isub>i"}; otherwise
we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the
- latter is because @{text "ty\<^isub>i"} is not part of the specified types
+ latter is because @{text "ty\<^isub>i"} is then not part of the specified types
and alpha-equivalence of any previously defined type is supposed to coincide
with equality. This lets us now define the premise for an empty binding
clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be
@@ -1984,7 +1986,7 @@
lemmas allow the user to deduce a property @{text "P"} by exhaustively
analysing how an element of a type, say @{text "ty\<AL>"}$_i$, can be
constructed (that means one case for each of the term-constructors in @{text
- "ty\<AL>"}$_i\,$). The lifted cases lemma for the type @{text
+ "ty\<AL>"}$_i\,$). The lifted cases lemma for a type @{text
"ty\<AL>"}$_i\,$ looks as follows
\begin{equation}\label{cases}
@@ -2231,7 +2233,7 @@
Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
with, for example, a pair, then this type-constraint will be propagated to
the premises. The main point is that if @{text "c"} is instantiated
- appropriately, then the user can mimic the usual `pencil-and-paper'
+ appropriately, then the user can mimic the usual convenient `pencil-and-paper'
reasoning employing the variable convention about bound and free variables
being distinct \cite{Urban08}.
@@ -2453,8 +2455,8 @@
holds. This allows us to use the implication from the strong cases
lemma, and we are done.
- Consequently, we can discharge all proof-obligations about having covered all
- cases. This completes the proof establishing that the weak induction principles imply
+ Consequently, we can discharge all proof-obligations about having `covered all
+ cases'. This completes the proof establishing that the weak induction principles imply
the strong induction principles. These strong induction principles have already proved
being very useful in practice, particularly for proving properties about
capture-avoiding substitution \cite{Urban08}.
@@ -2507,11 +2509,11 @@
\cite{BengtsonParow09,UrbanNipkow09}). Both
use the approach based on iterated single binders. Our experience with
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
- general binders described in this paper, but needs a cumbersome
- iteration with single binders. The resulting formal reasoning turned out to
- be rather unpleasant.
-
+ the need to `unbind' bound variables and the resulting formal reasoning turned out to
+ be rather unpleasant. In contrast, the unbinding can be
+ done in one step with our
+ general binders described in this paper.
+
The most closely related work to the one presented here is the Ott-tool by
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
@@ -2525,9 +2527,9 @@
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 atoms are removed from the support). We
- also showed that our specifications lift from `raw' types to types of
+ also showed that our specifications lift from `raw' terms to
alpha-equivalence classes. For this we have established (automatically) that every
- term-constructor and function defined for `raw' types
+ term-constructor and function defined for `raw' terms
is respectful w.r.t.~alpha-equivalence.
Although we were heavily inspired by the syntax of Ott, its definition of
@@ -2582,21 +2584,23 @@
\]\smallskip
\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 the Core-Haskell language from the Introduction. With the work
- presented in this paper we can define it formally as shown in
- Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
- a corresponding reasoning infrastructure. However we have found out that
- telescopes seem to not easily representable in our framework. The reason is that
- we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms.
- This requires restrictions, which class with the `global' scope of binders in
- telescopes. They can
- be represented in the framework described in \cite{WeirichYorgeySheard11} using an extension of
- the usual locally-nameless representation.
+ 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 the Core-Haskell
+ language from the Introduction. With the work presented in this
+ paper we can define it formally as shown in
+ Figure~\ref{nominalcorehas} and then Nominal Isabelle derives
+ automatically a corresponding reasoning infrastructure. However we
+ have found out that telescopes seem to not easily be representable
+ in our framework. The reason is that we need to be able to lift our
+ @{text bn}-functions to alpha-equated lambda-terms and therefore
+ need to restrict what these @{text bn}-functions can return.
+ Telescopes can be represented in the framework described in
+ \cite{WeirichYorgeySheard11} using an extension of the usual
+ locally-nameless representation.
\begin{figure}[p]
\begin{boxedminipage}{\linewidth}
@@ -2631,10 +2635,10 @@
\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"}\\
+ \;@{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 = []"}\\
@@ -2706,11 +2710,12 @@
definitions to equivariant functions (for them we can provide more
automation).
- There are some restrictions we imposed in this paper that can be lifted using
+ There are some restrictions we had
+ to impose in this paper that can be lifted using
a recent reimplementation \cite{Traytel12} of the datatype package for Isabelle/HOL, which
- is however not yet part of the stable distribution.
+ however is not yet part of the stable distribution.
This reimplementation allows nested
- datatype definitions would allow one to specify, for instance, the function kinds
+ datatype definitions and would allow one to specify, for instance, the function kinds
in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). We can
also use it to represent the @{text "Let"}-terms from the Introduction where
@@ -2723,10 +2728,10 @@
\]\smallskip
\noindent
- For this we have to represent the @{text "let"}-assignments as finite sets
+ For this we have to represent the @{text "Let"}-assignments as finite sets
of pair and a binding function that picks out the left components to be bound in @{text s}.
- One line of investigation is whether we can go beyond the
+ One line of future investigation is whether we can go beyond the
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
of atom sets (similarly for lists). It remains to be seen whether
--- a/LMCS-Paper/document/root.bib Fri Apr 20 15:28:35 2012 +0200
+++ b/LMCS-Paper/document/root.bib Fri Apr 20 15:29:40 2012 +0200
@@ -3,7 +3,7 @@
author = {D.~Traytel and A.~Popescu and J.~C.~Blanchette},
title = {{F}oundational, {C}ompositional ({C}o)datatypes for {H}igher-{O}rder
{L}ogic: {C}ategory {T}heory {A}pplied to {T}heorem {P}roving},
- note = {Submitted for publication},
+ note = {To appear in \emph{Proc.~of the 27th Symposium on Logic in Computer Science (LICS)}},
year = {2012}
}
@@ -112,12 +112,14 @@
pages = {173--184}
}
+
@Unpublished{chargueraud09,
- author = "A.~Chargu{\'e}raud",
- title = "{T}he {L}ocally {N}ameless {R}epresentation",
- Note = "To appear in Journal of Automated Reasoning."
+ author = "A.~Chargu{\'e}raud",
+ title = "{T}he {L}ocally {N}ameless {R}epresentation",
+ note = "To appear in \emph{Journal of Automated Reasoning}"
}
+
@article{NaraschewskiNipkow99,
author={W.~Naraschewski and T.~Nipkow},
title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}},
@@ -155,7 +157,7 @@
}
@Unpublished{Pitts04,
- author = {A.~Pitts},
+ author = {A.~M.~Pitts},
title = {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos},
note = {Unpublished notes for an invited talk given at CTCS},
year = {2004}