diff -r 6b1eea8dcdc0 -r f0028f13e532 Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 22 18:29:29 2010 +0100 +++ b/Paper/Paper.thy Mon Mar 22 18:29:57 2010 +0100 @@ -53,8 +53,8 @@ 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 are not captured - by iterating single binders. For example in the case of type-schemes we do not + Binding multiple variables has interesting properties that cannot be captured + easily by iterating single binders. For example in the case of type-schemes we do not like to make a distinction about the order of the bound variables. Therefore we would like to regard the following two type-schemes as alpha-equivalent % @@ -152,7 +152,7 @@ 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 specifications + for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications for $\mathtt{let}$s as follows \begin{center} @@ -165,7 +165,7 @@ \end{center} \noindent - where $assn$ is an auxiliary type representing a list of assignments + where $assn$ is an auxiliary type representing a list of assignments and $bn$ an auxiliary function identifying the variables to be bound by the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows @@ -176,9 +176,9 @@ \noindent The scope of the binding is indicated by labels given to the types, for example \mbox{$s\!::\!trm$}, and a binding clause, in this case - $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind all the names the function - $bn$ returns in $s$. This style of specifying terms and bindings is heavily - inspired by the syntax of the Ott-tool \cite{ott-jfp}. + $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the + function $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 @@ -189,8 +189,8 @@ \end{center} \noindent - where no clause for variables is given. Such specifications make sense in - the context of Coq's type theory (which Ott supports), but not in a HOL-based + where no clause for variables is given. Such specifications make some sense in + the context of Coq's type theory (which Ott supports), but not at al in a HOL-based theorem prover where every datatype must have a non-empty set-theoretic model. Another reason is that we establish the reasoning infrastructure @@ -253,7 +253,7 @@ \end{center} \noindent - We take as the starting point a definition of raw terms (being defined as a + We take as the starting point a definition of raw terms (defined as a datatype in Isabelle/HOL); identify then the alpha-equivalence classes in the type of sets of raw terms, according to our alpha-equivalence relation and finally define the new type as these @@ -263,23 +263,45 @@ The fact that we obtain an isomorphism between between the new type and the non-empty subset shows that the new type is a faithful representation of alpha-equated terms. - That is different for example in the representation of terms using the locally - nameless representation of binders: there are non-well-formed terms that need to + That is not the case for example in the representation of terms using the locally + nameless representation of binders \cite{McKinnaPollack99}: 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 + 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 reimplemented in Isabelle/HOL the quotient package described by Homeier - \cite{Homeier05}. Given that alpha is an equivalence relation, this package - allows us to automatically lift definitions and theorems involving raw terms - to definitions and theorems involving alpha-equated terms. This of course - only works if the definitions and theorems are respectful w.r.t.~alpha-equivalence. - Hence we will be able to lift, for instance, the function for free - variables of raw terms to alpha-equated terms (since this function respects - alpha-equivalence), but we will not be able to do this with a bound-variable - function (since it does not respect alpha-equivalence). As a result, each - lifting needs some respectfulness proofs which we automated.\medskip + we re-implemented in Isabelle/HOL the quotient package described by Homeier + \cite{Homeier05}. This package + allows us to lift definitions and theorems involving raw terms + to definitions and theorems involving alpha-equated terms. For example + if we define the free-variable function over 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 + + \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 is an equivalence relation, and the definitions and theorems + are respectful w.r.t.~alpha-equivalence. Hence we will not be able to lift this + a bound-variable function to alpha-equated terms (since it does not respect + alpha-equivalence). To sum up, every lifting needs proofs of some respectfulness + properties. These proofs we are able automate and therefore establish a + useful reasoning infrastructure for alpha-equated lambda terms.\medskip + \noindent {\bf Contributions:} We provide new definitions for when terms @@ -363,36 +385,34 @@ section {* General Binders *} text {* - In order to keep our work manageable we give need to give definitions - and perform proofs inside Isabelle wherever possible, as opposed to write - custom ML-code that generates them for each - instance of a term-calculus. To this end we will first consider pairs + In Nominal Isabelle the user is expected to write down a specification of a + term-calculus and a reasoning infrastructure is then automatically derived + from this specifcation (remember that Nominal Isabelle is a definitional + extension of Isabelle/HOL and cannot introduce new axioms). + - \begin{equation}\label{three} - \mbox{@{text "(as, x) :: (atom set) \ \"}} - \end{equation} - - \noindent - consisting of a set of atoms and an object of generic type. These pairs - are intended to represent the abstraction or binding of the set $as$ - in the body $x$ (similarly to type-schemes given in \eqref{tysch}). + 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 + end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. + These pairs are intended to represent the abstraction, or binding, of the set $as$ + in the body $x$. - The first question we have to answer is when we should consider pairs such as - $(as, x)$ and $(bs, y)$ as alpha-equivalent? (At the moment we are interested in + 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 of type \mbox{@{text "fv :: \ \ atom set"}}, then $x$ and $y$ + vacuous binders.) To answer this, we identify four conditions: {\it i)} given + a free-variable function $\fv$ of type \mbox{@{text "\ \ atom set"}}, then $x$ and $y$ need to have the same set of free variables; moreover there must be a permutation, - $p$ that {\it ii)} leaves the free variables $x$ and $y$ unchanged, - but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, + $p$ so that {\it ii)} it leaves the free variables $x$ and $y$ unchanged, + but {\it iii)} ``moves'' their bound names such that we obtain modulo a relation, say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that $p$ makes - the abstracted sets $as$ and $bs$ equal (since at the moment we do not want - that the sets $as$ and $bs$ differ on vacuous binders). These requirements can - be stated formally as follows + the abstracted sets $as$ and $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_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] + \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 "(p \ x) R y"}\\ @@ -401,20 +421,23 @@ \end{equation} \noindent - Alpha equivalence between such pairs is then the relation with the additional - existential quantification over $p$. Note that this relation is additionally - dependent on the free-variable function $\fv$ and the relation $R$. The reason - for this generality is that we want to use $\approx_{set}$ for both ``raw'' terms - and alpha-equated terms. In the latter case, $R$ can be replaced by equality $(op =)$ and - we are going to prove that $\fv$ will be equal to the support of $x$ and $y$. + Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where + 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 + them generically. The definition in \eqref{alphaset} does not make any distinction between the - order of abstracted variables. If we do want this then we can define alpha-equivalence - for pairs of the form \mbox{@{text "(as, x) :: (atom list) \ \"}} by + 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) \ \"} + as follows % \begin{equation}\label{alphalist} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] + \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 "(p \ x) R y"}\\ @@ -426,34 +449,65 @@ where $set$ is just 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 - allow vacuous binders, then we just need to drop the fourth condition in \eqref{alphaset} - and define + also allow vacuous binders, then we keep sets of binders, but drop the fourth + condition in \eqref{alphaset}: % - \begin{equation}\label{alphaset} + \begin{equation}\label{alphares} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] + \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 "(p \ x) R y"}\\ \end{array} \end{equation} - To get a feeling how these definitions pan out in practise consider the case of - abstracting names over types (like in type-schemes). For this we set $R$ to be - the equality and for $\fv(T)$ we define + \begin{exmple}\rm + It might be useful to consider some examples for how these definitions pan out in practise. + For this consider the case of abstracting a set of variables over types (as in type-schemes). + We set $R$ to be the equality and for $\fv(T)$ we define \begin{center} $\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$ \end{center} \noindent - Now reacall the examples in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}: it can be easily - checked that @{text "({x,y}, x \ y)"} and - @{text "({y,x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{ref}$ by taking $p$ to - be the swapping @{text "(x \ y)"}; but assuming @{text "x \ y"} then for instance - $([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, but leaves the type \mbox{@{text "x \ y"}} - unchanged. + Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily + checked that @{text "({x, y}, x \ y)"} and + @{text "({y, x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to + be the swapping @{term "(x \ y)"}. In case of @{text "x \ 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 + type \mbox{@{text "x \ y"}} unchanged. Again if @{text "x \ y"}, we have that + $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ by taking $p$ to be the identity permutation. + However $(\{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 + conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence + relations and equivariant: + + \begin{lemma} + {\it i)} Given the fact that $x\;R\;x$ holds, then + $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given + that @{text "(p \ x) R y"} implies @{text "(-p \ y) R x"}, then + $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies + $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given + that @{text "(p \ x) R y"} and @{text "(q \ y) R z"} implies + @{text "((q + p) \ x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ + and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies + $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given + @{text "(q \ x) R y"} implies @{text "(p \ (q \ x)) R (p \ y)"} and + @{text "p \ (fv x) = fv (p \ x)"} then @{text "p \ (fv y) = fv (p \ y)"}, then + $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies + $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star + (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$. + \end{lemma} + + \begin{proof} + All properties are by unfolding the definitions and simple calculations. + \end{proof} *} section {* Alpha-Equivalence and Free Variables *} @@ -467,6 +521,7 @@ \item finitely supported abstractions \item respectfulness of the bn-functions\bigskip \item binders can only have a ``single scope'' + \item all bindings must have the same mode \end{itemize} *} @@ -503,7 +558,11 @@ also for patiently explaining some of the finer points about the abstract definitions and about the implementation of the Ott-tool. + Lookup: Merlin paper by James Cheney; Mark Shinwell PhD + Future work: distinct list abstraction + + *}