# HG changeset patch # User Christian Urban # Date 1286885178 -3600 # Node ID 0cb0c88b2cad93912d1c2f9b4b4f0a9b19af979a # Parent e7cc033f72c72b423f7f7818814759af29d6c73b added a section about abstractions diff -r e7cc033f72c7 -r 0cb0c88b2cad Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Tue Oct 12 10:07:48 2010 +0100 +++ b/Pearl-jv/Paper.thy Tue Oct 12 13:06:18 2010 +0100 @@ -3,6 +3,7 @@ imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Atoms" + "../Nominal/Abs" "LaTeXsugar" begin @@ -60,7 +61,7 @@ al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a sort-respecting permutation operation defined over a countably infinite collection of sorted atoms. The atoms are used for representing variable names - that might be free or bound. Multiple sorts are necessary for being able to + that might be binding, bound or free. Multiple sorts are necessary for being able to represent different kinds of variables. For example, in the language Mini-ML there are bound term variables in lambda abstractions and bound type variables in type schemes. In order to be able to separate them, each kind of variables needs to be @@ -68,7 +69,8 @@ In our formalisation of the nominal logic work, we have to make a design decision about how to represent sorted atoms and sort-respecting permutations. One possibility - is to have separate types for the different kinds of atoms. With this one can represent + is to have separate types for the different kinds of atoms, say @{text "\\<^isub>1,\,\\<^isub>n"}. + With this design one can represent permutations as lists of pairs of atoms and the operation of applying a permutation to an object as the overloaded function @@ -94,18 +96,12 @@ @{text "b"}. For atoms of different type, the permutation operation is defined as @{text "\ \ c \ c"}. - -% Unfortunately, the type system of Isabelle/HOL is not a good fit for the way -% atoms and sorts are used in the original formulation of the nominal logic work. -% The reason is that one has to ensure that permutations are sort-respecting. -% This was done implicitly in the original nominal logic work \cite{Pitts03}. - - With the separate atom types and the list representation of permutations it - is impossible to state an ``ill-sorted'' permutation, since the type system - excludes lists containing atoms of different type. However, whenever we - need to generalise induction hypotheses by quantifying over permutations, we - have to build cumbersome quantifications like + is impossible in systems like Isabelle/HOL to state an ``ill-sorted'' + permutation, since the type system excludes lists containing atoms of + different type. However, a disadvantage is that whenever we need to + generalise induction hypotheses by quantifying over permutations, we have to + build quantifications like @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} @@ -130,21 +126,21 @@ \end{tabular}\hfill\numbered{fssequence} \end{isabelle} - - - - - - - + \noindent + Because of these disadvantages, we will use a single unified atom type to + represent atoms of different sorts. As a result, we have to deal with the + case that a swapping of two atoms is ill-sorted: we cannot rely anymore on + the type systems to exclude them. - An advantage of the - list representation is that the basic operations on permutations are already - defined in the list library: composition of two permutations (written @{text - "_ @ _"}) is just list append, and inversion of a permutation (written - @{text "_\<^sup>-\<^sup>1"}) is just list reversal. A disadvantage is that - permutations do not have unique representations as lists; we had to - explicitly identify permutations according to the relation + We also will not represent permutations as lists of pairs of atoms. An + advantage of this representation is that the basic operations on + permutations are already defined in Isabelle's list library: composition of + two permutations (written @{text "_ @ _"}) is just list append, and + inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just + list reversal. Another advantage is that there is a well-understood + induction principle for lists. A disadvantage, however, is that permutations + do not have unique representations as lists; we have to explicitly identify + them according to the relation \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -153,10 +149,13 @@ \end{tabular}\hfill\numbered{permequ} \end{isabelle} - When lifting the permutation operation to other types, for example sets, - functions and so on, we needed to ensure that every definition is - well-behaved in the sense that it satisfies the following three - \emph{permutation properties}: + \noindent + This is a problem when lifting the permutation operation to other types, for + example sets, functions and so on, we need to ensure that every definition + is well-behaved in the sense that it satisfies some + \emph{permutation properties}. In the list representation we need + to state these properties as follows: + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} @@ -167,116 +166,25 @@ \end{isabelle} \noindent - From these properties we were able to derive most facts about permutations, and - the type classes of Isabelle/HOL allowed us to reason abstractly about these - three properties, and then let the type system automatically enforce these - properties for each type. - - The major problem with Isabelle/HOL's type classes, however, is that they - support operations with only a single type parameter and the permutation - operations @{text "_ \ _"} used above in the permutation properties - contain two! To work around this obstacle, Nominal Isabelle - required the user to - declare up-front the collection of \emph{all} atom types, say @{text - "\\<^isub>1,\,\\<^isub>n"}. From this collection it used custom ML-code to - generate @{text n} type classes corresponding to the permutation properties, - whereby in these type classes the permutation operation is restricted to - - @{text [display,indent=10] "_ \ _ :: (\\<^isub>i \ \\<^isub>i) list \ \ \ \"} - - \noindent - This operation has only a single type parameter @{text "\"} (the @{text "\\<^isub>i"} are the - atom types given by the user). - - While the representation of permutations-as-lists solved the - ``sort-respecting'' requirement and the declaration of all atom types - up-front solved the problem with Isabelle/HOL's type classes, this setup - caused several problems for formalising the nominal logic work: First, - Nominal Isabelle had to generate @{text "n\<^sup>2"} definitions for the - permutation operation over @{text "n"} types of atoms. Second, whenever we - need to generalise induction hypotheses by quantifying over permutations, we - have to build cumbersome quantifications like - - @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} - - \noindent - where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. - The reason is that the permutation operation behaves differently for - every @{text "\\<^isub>i"}. Third, although the notion of support - - @{text [display,indent=10] "supp _ :: \ \ \ set"} - - \noindent - which we will define later, has a generic type @{text "\ set"}, it cannot be - used to express the support of an object over \emph{all} atoms. The reason - is again that support can behave differently for each @{text - "\\<^isub>i"}. This problem is annoying, because if we need to know in - a statement that an object, say @{text "x"}, is finitely supported we end up - with having to state premises of the form - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "finite ((supp x) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^isub>n set)"} - \end{tabular}\hfill\numbered{fssequence} - \end{isabelle} + where the last clause explicitly states that the permutation operation has + to produce the same result for related permutations. Moreover, permutations + as list do not satisfy the usual properties about groups. This means by + using this representation we will not be able to reuse the extensive + reasoning infrastructure in Isabelle about groups. Therefore, we will use + in this paper a unique representation for permutations by representing them + as functions from atoms to atoms. - \noindent - Sometimes we can avoid such premises completely, if @{text x} is a member of a - \emph{finitely supported type}. However, keeping track of finitely supported - types requires another @{text n} type classes, and for technical reasons not - all types can be shown to be finitely supported. - - The real pain of having a separate type for each atom sort arises, however, - from another permutation property - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} - iv) & @{text "\\<^isub>1 \ (\\<^isub>2 \ x) = (\\<^isub>1 \ \\<^isub>2) \ (\\<^isub>1 \ x)"} - \end{tabular} - \end{isabelle} + Using a single atom type to represent atoms of different sorts and + representing permutations as functions are not new ideas. The main + contribution of this paper is to show an example of how to make better + theorem proving tools by choosing the right level of abstraction for the + underlying theory---our design choices take advantage of Isabelle's type + system, type classes and reasoning infrastructure. The novel technical + contribution is a mechanism for dealing with ``Church-style'' lambda-terms + \cite{Church40} and HOL-based languages \cite{PittsHOL4} where variables and + variable binding depend on type annotations. - \noindent - where permutation @{text "\\<^isub>1"} has type @{text "(\ \ \) list"}, - @{text "\\<^isub>2"} type @{text "(\' \ \') list"} and @{text x} type @{text - "\"}. This property is needed in order to derive facts about how - permutations of different types interact, which is not covered by the - permutation properties @{text "i"}-@{text "iii"} shown in - \eqref{permprops}. The problem is that this property involves three type - parameters. In order to use again Isabelle/HOL's type class mechanism with - only permitting a single type parameter, we have to instantiate the atom - types. Consequently we end up with an additional @{text "n\<^sup>2"} - slightly different type classes for this permutation property. - - While the problems and pain can be almost completely hidden from the user in - the existing implementation of Nominal Isabelle, the work is \emph{not} - pretty. It requires a large amount of custom ML-code and also forces the - user to declare up-front all atom-types that are ever going to be used in a - formalisation. In this paper we set out to solve the problems with multiple - type parameters in the permutation operation, and in this way can dispense - with the large amounts of custom ML-code for generating multiple variants - for some basic definitions. The result is that we can implement a pleasingly - simple formalisation of the nominal logic work.\smallskip - - \noindent - {\bf Contributions of the paper:} Using a single atom type to represent - atoms of different sorts and representing permutations as functions are not - new ideas. The main contribution of this paper is to show an example of how - to make better theorem proving tools by choosing the right level of - abstraction for the underlying theory---our design choices take advantage of - Isabelle's type system, type classes, and reasoning infrastructure. - The novel - technical contribution is a mechanism for dealing with - ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages - \cite{PittsHOL4} where variables and variable binding depend on type - annotations. - - Therefore it was decided in earlier versions of Nominal Isabelle to use a - separate type for each sort of atoms and let the type system enforce the - sort-respecting property of permutations. Inspired by the work on nominal - unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also - implement permutations concretely as lists of pairs of atoms. - - + The paper is organised as follows *} section {* Sorted Atoms and Sort-Respecting Permutations *} @@ -286,26 +194,24 @@ represented by \emph{atoms}. As stated above, we need to have different \emph{sorts} of atoms to be able to bind different kinds of variables. A basic requirement is that there must be a countably infinite number of atoms - of each sort. Unlike in our earlier work, where we identified each sort with - a separate type, we implement here atoms to be + of each sort. We implement these atoms as *} datatype atom\ = Atom\ string nat text {* \noindent - whereby the string argument specifies the sort of the atom.\footnote{A similar - design choice was made by Gunter et al \cite{GunterOsbornPopescu09} - for their variables.} (The use type - \emph{string} is merely for convenience; any countably infinite type would work - as well.) - We have an auxiliary function @{text sort} that is defined as @{thm - sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of - atoms and every sort @{text s} the property: - + whereby the string argument specifies the sort of the atom.\footnote{A + similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} + for their variables.} (The use type \emph{string} is merely for + convenience; any countably infinite type would work as well.) We have an + auxiliary function @{text sort} that is defined as @{thm + sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} + of atoms and every sort @{text s} the property: + \begin{proposition}\label{choosefresh} - @{text "If finite X then there exists an atom a such that - sort a = s and a \ X"}. + @{text "For a finite set of atoms S, there exists an atom a such that + sort a = s and a \ S"}. \end{proposition} For implementing sort-respecting permutations, we use functions of type @{typ @@ -341,7 +247,7 @@ \noindent but since permutations are required to respect sorts, we must carefully consider what happens if a user states a swapping of atoms with different - sorts. In earlier versions of Nominal Isabelle, we avoided this problem by + sorts. In early versions of Nominal Isabelle, we avoided this problem by using different types for different sorts; the type system prevented users from stating ill-sorted swappings. Here, however, definitions such as\footnote{To increase legibility, we omit here and in what follows the @@ -946,6 +852,218 @@ *} +section {* An Abstraction Type *} + +text {* + To that end, we will consider + first pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. These pairs + are intended to represent the abstraction, or binding, of the set of atoms @{text + "as"} in the body @{text "x"}. + + The first question we have to answer is when two pairs @{text "(as, x)"} and + @{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in + the notion of $\alpha$-equivalence that is \emph{not} preserved by adding + vacuous binders.) To answer this question, we identify four conditions: {\it (i)} + given a free-atom function @{text "fa"} of type \mbox{@{text "\ \ atom + set"}}, then @{text x} and @{text y} need to have the same set of free + atoms; moreover there must be a permutation @{text p} such that {\it + (ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but + {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation, + say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)} + @{text p} makes the sets of abstracted atoms @{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@ {\hspace{4mm}}r} + \multicolumn{3}{l}{@{text "(as, x) \set R fa p (bs, y)"}\hspace{2mm}@{text "\"}}\\[1mm] + & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\ + @{text "\"} & @{term "(fa(x) - as) \* p"} & \mbox{\it (ii)}\\ + @{text "\"} & @{text "(p \ x) R y"} & \mbox{\it (iii)}\\ + @{text "\"} & @{term "(p \ as) = bs"} & \mbox{\it (iv)}\\ + \end{array} + \end{equation} + + \noindent + Note that this relation depends on the permutation @{text + "p"}; $\alpha$-equivalence between two pairs is then the relation where we + existentially quantify over this @{text "p"}. Also note that the relation is + dependent on a free-atom function @{text "fa"} and a relation @{text + "R"}. The reason for this extra generality is that we will use + $\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In + the latter case, @{text R} will be replaced by equality @{text "="} and we + will prove that @{text "fa"} is equal to @{text "supp"}. + + It might be useful to consider first some examples about how these definitions + of $\alpha$-equivalence pan out in practice. For this consider the case of + abstracting a set of atoms over types (as in type-schemes). We set + @{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we + define + + \begin{center} + @{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \ T\<^isub>2) = fa(T\<^isub>1) \ fa(T\<^isub>2)"} + \end{center} + + \noindent + 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 $\alpha$-equivalent according to + $\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to + be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then @{text + "([x, y], x \ y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \ y)"} + since there is no permutation that makes the lists @{text "[x, y]"} and + @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \ y"}} + unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$ + @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity + permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} + $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no + permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal + (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be + shown that all three notions of $\alpha$-equivalence coincide, if we only + abstract a single atom. + + In the rest of this section we are going to introduce three abstraction + types. For this we define + % + \begin{equation} + @{term "abs_set (as, x) (bs, x) \ \p. alpha_set (as, x) equal supp p (bs, x)"} + \end{equation} + + \noindent + (similarly for $\approx_{\,\textit{abs\_res}}$ + and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence + relations and equivariant. + + \begin{lemma}\label{alphaeq} + The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ + and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term + "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \ as, p \ x) (p \ + bs, p \ y)"} (similarly for the other two relations). + \end{lemma} + + \begin{proof} + Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have + a permutation @{text p} and for the proof obligation take @{term "-p"}. In case + of transitivity, we have two permutations @{text p} and @{text q}, and for the + proof obligation use @{text "q + p"}. All conditions are then by simple + calculations. + \end{proof} + + \noindent + This lemma allows us to use our quotient package for introducing + new types @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} + representing $\alpha$-equivalence classes of pairs of type + @{text "(atom set) \ \"} (in the first two cases) and of type @{text "(atom list) \ \"} + (in the third case). + The elements in these types will be, respectively, written as: + + \begin{center} + @{term "Abs_set as x"} \hspace{5mm} + @{term "Abs_res as x"} \hspace{5mm} + @{term "Abs_lst as x"} + \end{center} + + \noindent + indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will + call the types \emph{abstraction types} and their elements + \emph{abstractions}. The important property we need to derive is the support of + abstractions, namely: + + \begin{theorem}[Support of Abstractions]\label{suppabs} + Assuming @{text x} has finite support, then\\[-6mm] + \begin{center} + \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + %@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\ + %@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\ + %@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]} + \end{tabular} + \end{center} + \end{theorem} + + \noindent + Below we will show the first equation. The others + follow by similar arguments. By definition of the abstraction type @{text "abs_set"} + we have + % + \begin{equation}\label{abseqiff} + %@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; + %@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} + \end{equation} + + \noindent + and also + % + \begin{equation}\label{absperm} + @{thm permute_Abs[no_vars]} + \end{equation} + + \noindent + The second fact derives from the definition of permutations acting on pairs + \eqref{permute} and $\alpha$-equivalence being equivariant + (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show + the following lemma about swapping two atoms in an abstraction. + + \begin{lemma} + %@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]} + \end{lemma} + + \begin{proof} + This lemma is straightforward using \eqref{abseqiff} and observing that + the assumptions give us @{term "(a \ b) \ (supp x - as) = (supp x - as)"}. + Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). + \end{proof} + + \noindent + Assuming that @{text "x"} has finite support, this lemma together + with \eqref{absperm} allows us to show + % + \begin{equation}\label{halfone} + %@ {thm abs_supports(1)[no_vars]} + \end{equation} + + \noindent + which by Property~\ref{supportsprop} gives us ``one half'' of + Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish + it, we use a trick from \cite{Pitts04} and first define an auxiliary + function @{text aux}, taking an abstraction as argument: + % + \begin{center} + @{thm supp_set.simps[THEN eq_reflection, no_vars]} + \end{center} + + \noindent + Using the second equation in \eqref{equivariance}, we can show that + @{text "aux"} is equivariant (since @{term "p \ (supp x - as) = + (supp (p \ x)) - (p \ as)"}) and therefore has empty support. + This in turn means + % + \begin{center} + @{term "supp (supp_gen (Abs_set as x)) \ supp (Abs_set as x)"} + \end{center} + + \noindent + using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, + we further obtain + % + \begin{equation}\label{halftwo} + %@ {thm (concl) supp_abs_subset1(1)[no_vars]} + \end{equation} + + \noindent + since for finite sets of atoms, @{text "bs"}, we have + @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. + Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes + Theorem~\ref{suppabs}. + + The method of first considering abstractions of the + form @{term "Abs_set as x"} etc is motivated by the fact that + we can conveniently establish at the Isabelle/HOL level + properties about them. It would be + laborious to write custom ML-code that derives automatically such properties + for every term-constructor that binds some atoms. Also the generality of + the definitions for $\alpha$-equivalence will help us in the next section. +*} + + section {* Concrete Atom Types *} text {* diff -r e7cc033f72c7 -r 0cb0c88b2cad Pearl-jv/ROOT.ML --- a/Pearl-jv/ROOT.ML Tue Oct 12 10:07:48 2010 +0100 +++ b/Pearl-jv/ROOT.ML Tue Oct 12 13:06:18 2010 +0100 @@ -1,6 +1,7 @@ no_document use_thys ["../Nominal-General/Nominal2_Base", "../Nominal-General/Nominal2_Eqvt", - "../Nominal-General/Atoms", + "../Nominal-General/Atoms", + "../Nominal/Abs", "LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file