nominal2: comparison LMCS-Paper/Paper.thy

equal deleted inserted replaced

-:aa1ba91ed1ff
+:95ff21cda33c
 \noindent
 Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to
 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
+for alpha-equated type-schemes. With the unbinding relation
-definition in place we can formally define when a type is an instance of a type-scheme as follows:
+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"}
 \]\smallskip
 This means there exists a list of type-variables @{text xs} and a type @{text T'} to which
 the type-scheme @{text S} unbinds, and there exists a substitution @{text "\<sigma>"} whose domain is
 @{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.
 Binding multiple variables has interesting properties that cannot be captured
 unions of atom sets or appended atom lists (case @{text ACons'}). This
 restriction will simplify some automatic definitions and proofs later on.
 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
 constructor, but bodies of binding clauses can only occur in a
 single one. Binding clauses come in three modes: \isacommand{binds},
 binders can occur in more than one binding clause and only have to
 respect the binding mode (i.e.~be of the right type). Deep binders
 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
+atoms that are not mentioned in any binding clause.
-simplify our definitions of free atoms and alpha-equivalence, we
+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
 given by the user, we add implicitly a special \emph{empty} binding
 clause, written \isacommand{binds}~@{term
 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
 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"}}
 \]\smallskip
 The alpha-equivalence relations are defined as inductive predicates
 having a single clause for each term-constructor. Assuming a
 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
 clause are. To understand better what the general pattern is, let us first
 treat the special instance where @{text "bc\<^isub>i"} is the empty binding clause
 \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)"}
 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"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of the @{text
-"z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such
+"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
 \begin{equation}\label{rempty}
 \mbox{@{text "R \<equiv> (R\<^isub>1,\<dots>, R\<^isub>q)"}}
 \noindent
 with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding
 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
 unfolded to the series of premises
 We can also 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 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}
 \infer{P}
 {\begin{array}{l}
 line). In order to see how an instantiation for @{text "c"} in the
 conclusion `controls' the premises, one has to take into account that
 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}.
 In what follows we will show that the weak induction principle in
 \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for
 \noindent
 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
+Consequently,  we can discharge all proof-obligations about having `covered all
-cases. This completes the proof establishing that the weak induction principles imply
+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}.
 *}
 performed in older
 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W
 \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
+the need to `unbind' bound variables and the resulting formal reasoning turned out to
-general binders described in this paper, but needs a cumbersome
+be rather unpleasant. In contrast, the unbinding can be
-iteration with single binders. The resulting formal reasoning turned out to
+done in one step with our
-be rather unpleasant.
+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
 from specifications of term-calculi involving general binders. For a subset
 of the specifications Ott can also generate theorem prover code using a `raw'
 specified in Ott.  This definition is rather different from ours, not using
 any nominal techniques.  To our knowledge there is no concrete mathematical
 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
 alpha-equi\-valence is unsuitable for our extension of Nominal
 Isabelle. First, it is far too complicated to be a basis for automated
 @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
 \end{tabular}}
 \]\smallskip
 \noindent
-and therefore need the extra generality to be able to distinguish between
+and therefore need the extra generality to be able to distinguish
-both specifications.  Because of how we set up our definitions, we also had
+between both specifications.  Because of how we set up our
-to impose some restrictions (like a single binding function for a deep
+definitions, we also had to impose some restrictions (like a single
-binder) that are not present in Ott. Our expectation is that we can still
+binding function for a deep binder) that are not present in Ott. Our
-cover many interesting term-calculi from programming language research, for
+expectation is that we can still cover many interesting term-calculi
-example the Core-Haskell language from the Introduction. With the work
+from programming language research, for example the Core-Haskell
-presented in this paper we can define it formally as shown in
+language from the Introduction. With the work presented in this
-Figure~\ref{nominalcorehas} and then Nominal Isabelle derives automatically
+paper we can define it formally as shown in
-a corresponding reasoning infrastructure. However we have found out that
+Figure~\ref{nominalcorehas} and then Nominal Isabelle derives
-telescopes seem to not easily representable in our framework. The reason is that
+automatically a corresponding reasoning infrastructure. However we
-we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms.
+have found out that telescopes seem to not easily be representable
-This requires restrictions, which class with the `global' scope of binders in
+in our framework.  The reason is that we need to be able to lift our
-telescopes. They can
+@{text bn}-functions to alpha-equated lambda-terms and therefore
-be represented in the framework described in \cite{WeirichYorgeySheard11} using an extension of
+need to restrict what these @{text bn}-functions can return.
-the usual locally-nameless representation.
+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}
 \small
 \begin{tabular}{l}
 \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 :: pat \<Rightarrow> atom list"}~\isacommand{and}\\
-@{text "bv\<^isub>1 :: vt_lst \<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>2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-@{text "bv\<^isub>3 :: tvck_lst \<Rightarrow> atom list"}\\
+\;@{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 = []"}\\
 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).
-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
 the order of @{text "let"}-assignments does not matter. This means we can represent @{text "Let"}s
 such that the following two terms are equal
 @{text "Let x\<^isub>1 = t\<^isub>1 and x\<^isub>2 = t\<^isub>2 in s"} \;\;=\;\;
 @{text "Let x\<^isub>2 = t\<^isub>2 and x\<^isub>1 = t\<^isub>1 in s"}
 \]\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
 properties like

changeset 3162	95ff21cda33c
parent 3160	603a36f19bfe