nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:b7e19f16bcd0
+:99cee15cb5ff
 As a result, we provide three general binding mechanisms each of which binds multiple
 variables at once, and let the user chose which one is intended when formalising a
 programming language calculus.
 By providing these general binding mechanisms, however, we have to work around
-a problem that has been pointed out by Pottier in \cite{Pottier06}: in
+a problem that has been pointed out by Pottier in \cite{Pottier06} and Cheney in
+\cite{Cheney05}: in
 $\mathtt{let}$-constructs of the form
 %
 \begin{center}
 $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
 \end{center}
 \end{center}
 \noindent
 where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound
 in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$}
-would be a perfectly legal instance. To exclude such terms an additional
+would be a perfectly legal instance. To exclude such terms, an additional
 predicate about well-formed terms is needed in order to ensure that the two
 lists are of equal length. This can result into very messy reasoning (see
 for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
 for $\mathtt{let}$s as follows
 %
 $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the
 function call $bn\,(a)$ returns.  This style of specifying terms and bindings is
 heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 However, we will not be able to deal with all specifications that are
-allowed by Ott. One reason is that Ott allows ``empty'' specifications
+allowed by Ott. One reason is that Ott lets the user to specify ``empty''
-like
+types like
 \begin{center}
 $t ::= t\;t \mid \lambda x. t$
 \end{center}
 \noindent
-where no clause for variables is given. Such specifications make some sense in
+where no clause for variables is given. Arguably, such specifications make
-the context of Coq's type theory (which Ott supports), but not at all in a HOL-based
+some sense in the context of Coq's type theory (which Ott supports), but not
-environment where every datatype must have a non-empty set-theoretic model.
+at all in a HOL-based environment where every datatype must have a non-empty
+set-theoretic model.
 Another reason is that we establish the reasoning infrastructure
 for alpha-\emph{equated} terms. In contrast, Ott produces  a reasoning
 infrastructure in Isabelle/HOL for
 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
 and the raw terms produced by Ott use names for bound variables,
 there is a key difference: working with alpha-equated terms means that the
-two type-schemes with $x$, $y$ and $z$ being distinct
+two type-schemes (with $x$, $y$ and $z$ being distinct)
 \begin{center}
 $\forall \{x\}. x \rightarrow y  \;=\; \forall \{x, z\}. x \rightarrow y$
 \end{center}
 \noindent
-are not just alpha-equal, but actually equal. As a
+are not just alpha-equal, but actually \emph{equal}. As a
 result, we can only support specifications that make sense on the level of
 alpha-equated terms (offending specifications, which for example bind a variable
 according to a variable bound somewhere else, are not excluded by Ott, but we
 have to).  Our
 insistence on reasoning with alpha-equated terms comes from the wealth of
 definable as datatype in Isabelle/HOL and the fact that our relation for
 alpha-equivalence is indeed an equivalence relation).
 The fact that we obtain an isomorphism between the new type and the non-empty
 subset shows that the new type is a faithful representation of alpha-equated terms.
-That is not the case for example in the representation of terms using the locally
+That is not the case for example for terms using the locally
 nameless representation of binders \cite{McKinnaPollack99}: in this representation
 there are ``junk'' terms that need to
 be excluded by reasoning about a well-formedness predicate.
 The problem with introducing a new type in Isabelle/HOL is that in order to be useful,
 a reasoning infrastructure needs to be ``lifted'' from the underlying subset to
 the new type. This is usually a tricky and arduous task. To ease it,
 we re-implemented in Isabelle/HOL the quotient package described by Homeier
-\cite{Homeier05}. This package
+\cite{Homeier05} for the HOL4 system. This package
 allows us to  lift definitions and theorems involving raw terms
-to definitions and theorems involving alpha-equated, terms. For example
+to definitions and theorems involving alpha-equated terms. For example
-if we define the free-variable function over lambda terms
+if we define the free-variable function over raw lambda-terms
 \begin{center}
 $\fv(x) = \{x\}$\hspace{10mm}
 $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm]
 $\fv(\lambda x.t) = \fv(t) - \{x\}$
 \end{center}
 \noindent
 then with not too great effort we obtain a function $\fv_\alpha$
-operating on quotients, or alpha-equivalence classes of terms, as follows
+operating on quotients, or alpha-equivalence classes of lambda-terms. This
+function is characterised by the equations
 \begin{center}
 $\fv_\alpha(x) = \{x\}$\hspace{10mm}
 $\fv_\alpha(t_1\;t_2) = \fv_\alpha(t_1) \cup \fv_\alpha(t_2)$\\[1mm]
 $\fv_\alpha(\lambda x.t) = \fv_\alpha(t) - \{x\}$
 \end{center}
 \noindent
 (Note that this means also the term-constructors for variables, applications
 and lambda are lifted to the quotient level.)  This construction, of course,
-only works if alpha-equivalence is an equivalence relation, and the
+only works if alpha-equivalence is an equivalence relation, and the lifted
-definitions and theorems are respectful w.r.t.~alpha-equivalence.  Hence we
+definitions and theorems are respectful w.r.t.~alpha-equivalence.  Accordingly, we
 will not be able to lift a bound-variable function to alpha-equated terms
 (since it does not respect alpha-equivalence). To sum up, every lifting of
 theorems to the quotient level needs proofs of some respectfulness
 properties. In the paper we show that we are able to automate these
 proofs and therefore can establish a reasoning infrastructure for
 of what follows. Two central notions in the nominal logic work are sorted
 atoms and sort-respecting permutations of atoms. The sorts can be used to
 represent different kinds of variables, such as term- and type-variables in
 Core-Haskell, and it is assumed that there is an infinite supply of atoms
 for each sort. However, in order to simplify the description, we shall
-assume in what follows that there is only a single sort of atoms.
+assume in what follows that there is only one sort of atoms.
 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[display,indent=5] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+@{text[display,indent=5] "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
 \noindent
-with a generic type in which @{text "\<alpha>"} stands for the type of atoms
+with a generic type in which @{text "\<beta>"} stands for the type of the object
-and @{text "\<beta>"} for the type of the object on which the permutation
+on which the permutation
-acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},
+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 for products, lists, sets, functions, booleans etc
-(see \cite{HuffmanUrban10}).
+(see \cite{HuffmanUrban10}). In the nominal logic work, concrete
+permutations are usually build up from swappings, written as @{text "(a b)"},
+which are permutations that behave as follows:
+%
+@{text[display,indent=5] "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
 The most original aspect of the nominal logic work of Pitts is a general
 definition for the notion of ``the set of free variables of an object @{text
 "x"}''.  This notion, written @{term "supp x"}, is general in the sense that
 it applies not only to lambda-terms alpha-equated or not, but also to lists,
 products, sets and even functions. The definition depends only on the
 permutation operation and on the notion of equality defined for the type of
 @{text x}, namely:
+%
 @{thm[display,indent=5] supp_def[no_vars, THEN eq_reflection]}
 \noindent
 There is also the derived notion for when an atom @{text a} is \emph{fresh}
 for an @{text x}, defined as
+%
 @{thm[display,indent=5] fresh_def[no_vars]}
 \noindent
 We also use for sets of atoms the abbreviation
 @{thm (lhs) fresh_star_def[no_vars]} defined as
 section {* General Binders *}
 text {*
 In Nominal Isabelle, the user is expected to write down a specification of a
 term-calculus and then a reasoning infrastructure is automatically derived
-from this specifcation (remember that Nominal Isabelle is a definitional
+from this specification (remember that Nominal Isabelle is a definitional
 extension of Isabelle/HOL, which does not introduce any new axioms).
 In order to keep our work manageable, we will wherever possible state
 definitions and perform proofs inside Isabelle, as opposed to write custom
-ML-code that generates them for each instance of a term-calculus. To that
+ML-code that generates them anew for each specification. To that
 end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}.
-These pairs are intended to represent the abstraction, or binding, of the set $as$
+These pairs are intended to represent the abstraction, or binding, of the set @{text "as"}
-in the body $x$.
+in the body @{text "x"}.
 The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are
 alpha-equivalent? (At the moment we are interested in
 the notion of alpha-equivalence that is \emph{not} preserved by adding
 vacuous binders.) To answer this, we identify four conditions: {\it i)} given
-a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then $x$ and $y$
+a free-variable function $\fv$ of type \mbox{@{text "\<beta> \<Rightarrow> atom set"}}, then @{text x} and @{text y}
-need to have the same set of free variables; moreover there must be a permutation,
+need to have the same set of free variables; moreover there must be a permutation
-$p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged,
+@{text p}  such that {\it ii)} it leaves the free variables of @{text x} and @{text y} unchanged,
-but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation,
+but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
-say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes
+say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that @{text p} makes
-the abstracted sets $as$ and $bs$ equal. The requirements {\it i)} to {\it iv)} can
+the abstracted sets @{text as} and @{text bs} equal. The requirements {\it i)} to {\it iv)} can
 be stated formally as follows:
 %
 \begin{equation}\label{alphaset}
 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
 \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
 & @{text "fv(x) - as = fv(y) - bs"}\\
-\wedge     & @{text "fv(x) - as #* p"}\\
+\wedge     & @{text "(fv(x) - as) #* p"}\\
 \wedge     & @{text "(p \<bullet> x) R y"}\\
 \wedge     & @{text "(p \<bullet> as) = bs"}\\
 \end{array}
 \end{equation}
 we existentially quantify over this $p$.
 Also note that the relation is dependent on a free-variable function $\fv$ and a relation
 $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both
 ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by
 equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support
-of $x$ and $y$. To have these parameters means, however, we can derive properties about
+of $x$ and $y$.
-them generically.
 The definition in \eqref{alphaset} does not make any distinction between the
 order of abstracted variables. If we want this, then we can define alpha-equivalence
 for pairs of the form \mbox{@{text "(as, x)"}} with type @{text "(atom list) \<times> \<beta>"}
 as follows
 %
 \begin{equation}\label{alphalist}
 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
 \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
 & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\
-\wedge     & @{text "fv(x) - (set as) #* p"}\\
+\wedge     & @{text "(fv(x) - set as) #* p"}\\
 \wedge     & @{text "(p \<bullet> x) R y"}\\
 \wedge     & @{text "(p \<bullet> as) = bs"}\\
 \end{array}
 \end{equation}
 \noindent
-where $set$ is just the function that coerces a list of atoms into a set of atoms.
+where $set$ is the function that coerces a list of atoms into a set of atoms.
 If we do not want to make any difference between the order of binders and
 also allow vacuous binders, then we keep sets of binders, but drop the fourth
 condition in \eqref{alphaset}:
 %
 \begin{equation}\label{alphares}
 \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
 \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm]
 & @{text "fv(x) - as = fv(y) - bs"}\\
-\wedge     & @{text "fv(x) - as #* p"}\\
+\wedge     & @{text "(fv(x) - as) #* p"}\\
 \wedge     & @{text "(p \<bullet> x) R y"}\\
 \end{array}
 \end{equation}
 \begin{exmple}\rm
 \noindent
 Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily
 checked that @{text "({x, y}, x \<rightarrow> y)"} and
 @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to
-be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"} then
+be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then
 $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that
-makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and in addition leaves the
+makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the
-type \mbox{@{text "x \<rightarrow> y"}} unchanged. Again if @{text "x \<noteq> y"}, we have that
+type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another examples is
-$(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation.
+$(\{x\}, x) \approx_{res} (\{x,y\}, x)$ which holds by taking $p$ to be the identity permutation.
-However $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
+However, if @{text "x \<noteq> y"}, then
+$(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes
 the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$).
 \end{exmple}
 \noindent
 Let $\star$ range over $\{set, res, list\}$. We prove next under which
 *}
 section {* Alpha-Equivalence and Free Variables *}
 text {*
-The syntax of a specification for a term-calculus in Nominal Isabelle is
+Our specifications for term-calculi are heavily
-heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a
+inspired by the syntax of the Ott-tool \cite{ott-jfp}. A specification is
-collection of (possibly mutual recursive) type declarations, say
+a collection of (possibly mutual recursive) type declarations, say
-$ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
+$ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and an
-collection of associated binding function declarations, say
+associated collection of binding function declarations, say
-$bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically
+$bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically written as
-written as follows:
+follows:
 \begin{center}
 \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
-types \mbox{declaration part} &
+type \mbox{declaration part} &
 $\begin{cases}
 \mbox{\begin{tabular}{l}
 \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\
 \isacommand{and} $ty_{\alpha{}2} = \ldots$\\
 $\ldots$\\
 \isacommand{and} $ty_{\alpha{}n} = \ldots$\\
 \end{tabular}}
 \end{cases}$\\
-binding \mbox{functions part} &
+binding \mbox{function part} &
 $\begin{cases}
 \mbox{\begin{tabular}{l}
 \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$
 $\ldots$\\
 \isacommand{where}\\
 \end{cases}$\\
 \end{tabular}
 \end{center}
 \noindent
-Each type declaration $ty_{\alpha{}i}$ consists of a collection of
+Every type declaration $ty_{\alpha{}i}$ consists of a collection of
 term-constructors, each of which comes with a list of labelled
-types that indicate the types of the arguments of the term-constructor,
+types that indicate the types of the arguments of the term-constructor.
-like
+For example for a term-constructor $C_{\alpha}$ we might have
 \begin{center}
 $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$
 \end{center}
 \noindent
-The labels are optional and can be used in the (possibly empty) list of binding clauses.
+The labels are optional and can be used in the (possibly empty) list of \emph{binding clauses}.
-These clauses indicate the binders and the scope of the binders in a term-constructor. They
+These clauses indicate  the binders and the scope of the binders in a term-constructor.
-are of the form
+They come in three forms
 \begin{center}
-\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}
+\begin{tabular}{l}
-\end{center}
+\isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label}\\
+\isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it label}\\
-\noindent
+\isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it label}\\
-whereby we distinguish between \emph{shallow} binders and \emph{deep} binders.
+\end{tabular}
-Shallow binders are just of the form \isacommand{bind}\; {\it label}\;
+\end{center}
-\isacommand{in}\; {\it another\_label}. The only restriction on shallow binders
-is that the {\it label} must refer to either a type which is single atom or
+\noindent
-to a type which is a finite set of atoms. For example the specification of
+whereby we also distinguish between \emph{shallow} binders and \emph{deep} binders.
-lambda-terms and type-schemes use them:
+Shallow binders are of the form \isacommand{bind}\; {\it label}\;
+\isacommand{in}\; {\it another\_label} (similar the other forms). The restriction
+we impose on shallow binders
+is that the {\it label} must either refer to a type that is an atom type or
+to a type that is a finite set or list of an atom type. For example the specifications of
+lambda-terms and type-schemes use shallow binders (where \emph{name} is an atom type):
 \begin{center}
 \begin{tabular}{@ {}cc@ {}}
 \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
 \isacommand{nominal\_datatype} {\it lam} =\\
 \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
 \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
 \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
-\hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+\hspace{21mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
 \end{tabular} &
 \begin{tabular}{@ {}l@ {}}
 \isacommand{nominal\_datatype} {\it ty} =\\
 \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
 \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
-\isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
+\isacommand{and} {\it tsc} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
-\hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\
+\hspace{22mm}\isacommand{bind\_res} {\it xs} \isacommand{in} {\it T}\\
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
-A specification of a term-calculus in Nominal Isabell is very similar to
+A \emph{deep} binder uses an auxiliary binding function that picks out the atoms
+that are bound in one or more arguments. This binding function returns either
+a set of atoms (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a
+list of atoms (for \isacommand{bind}). Such binding functions can be defined
+by primitive recursion over the corresponding type. They are defined by equations
+included in the binding function part of the scheme given above.
+For the moment we
+adopt the restriction of the Ott-tool that binding functions can only return
+the empty set, a singleton set of atoms or unions of atom sets. For example
+over the type for which they specify the bound atoms.
+\noindent
+A specification of a term-calculus in Nominal Isabelle is very similar to
 the usual datatype definition of Isabelle/HOL:
 Because of the problem Pottier pointed out in \cite{Pottier06}, the general
 binders from the previous section cannot be used directly to represent w

changeset 1617	99cee15cb5ff
parent 1613	98b53cd05deb
child 1619	373cd788d327