diff -r 0368aef38e6a -r 8466fe2216da Paper/Paper.thy --- a/Paper/Paper.thy Mon Mar 22 11:55:29 2010 +0100 +++ b/Paper/Paper.thy Mon Mar 22 16:22:07 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 @@ -467,6 +489,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 +526,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 + + *}