# HG changeset patch # User Christian Urban # Date 1302416035 -28800 # Node ID 64a03564bc24de07f11d43752305eb70f23a13a6 # Parent 8f833ebc4b58e6a76314984bff9777ca1e3d3910 more paper diff -r 8f833ebc4b58 -r 64a03564bc24 Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Sun Apr 10 07:41:52 2011 +0800 +++ b/Pearl-jv/Paper.thy Sun Apr 10 14:13:55 2011 +0800 @@ -351,6 +351,7 @@ \end{isabelle} \noindent + and will be defined over the hierarchie of types. Isabelle/HOL allows us to give a definition of this operation for `base' types, such as atoms, permutations, booleans and natural numbers: @@ -388,9 +389,8 @@ \end{isabelle} \noindent - From these properties and the laws about groups - (\ref{grouplaws}.{\it iv }) follows that a permutation and its inverse - cancel each other. That is + From these properties and law (\ref{grouplaws}.{\it iv}) about groups + follows that a permutation and its inverse cancel each other. That is \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -478,10 +478,11 @@ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}[b]{@ {}rcl} - @{text "0 \ \'"} & @{text "\"} & @{text "0 + \' - 0 = \'"}\\ + @{text "0 \ \'"} & @{text "\"} & @{text "0 + \' - 0 = \'"}\smallskip\\ @{text "(\\<^isub>1 + \\<^isub>2) \ \'"} & @{text "\"} & @{text "(\\<^isub>1 + \\<^isub>2) + \' - (\\<^isub>1 + \\<^isub>2)"}\\ & @{text "="} & @{text "(\\<^isub>1 + \\<^isub>2) + \' - \\<^isub>2 - \\<^isub>1"}\\ - & @{text "="} & @{text "\\<^isub>1 + (\\<^isub>2 + \' - \\<^isub>2) - \\<^isub>1"} @{text "\"} @{text "\\<^isub>1 \ \\<^isub>2 \ \'"} + & @{text "="} & @{text "\\<^isub>1 + (\\<^isub>2 + \' - \\<^isub>2) - \\<^isub>1"}\\ + & @{text "\"} & @{text "\\<^isub>1 \ \\<^isub>2 \ \'"} \end{tabular}\hfill\qed \end{isabelle} \end{proof} @@ -491,9 +492,10 @@ text {* An important notion in the nominal logic work is - \emph{equivariance}. In order to prove properties about this notion, - let us first define \emph{HOL-terms}. They are given - by the grammar + \emph{equivariance}. It will enable us to characterise how + permutations act upon compound statements in HOL by analysing how + these statements are constructed. To do so, let us first define + \emph{HOL-terms}. They are given by the grammar \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \x. t"} @@ -501,26 +503,26 @@ \end{isabelle} \noindent - whereby @{text c} stands for constant symbols, or short constants, and - @{text x} for variables. We assume HOL-terms are fully typed, but for the - sake of greater legibility we leave the typing information implicit. We - also assume the usual notions for free and bound variables of a HOL-term. - It is custom in HOL to regard terms equal modulo alpha-, beta- and - eta-equivalence. + whereby @{text c} stands for constants and @{text x} for + variables. We assume HOL-terms are fully typed, but for the sake of + greater legibility we leave the typing information implicit. We + also assume the usual notions for free and bound variables of a + HOL-term. Furthermore, it is custom in HOL to regard terms as equal + modulo alpha-, beta- and eta-equivalence. - An equivariant HOL-term is one that is invariant under the - permutation operation. This notion can be defined in Isabelle/HOL + An \emph{equivariant} HOL-term is one that is invariant under the + permutation operation. This can be defined in Isabelle/HOL as follows: \begin{definition}[Equivariance]\label{equivariance} - A HOL-term @{text t} with permutation type is \emph{equivariant} provided + A HOL-term @{text t} is \emph{equivariant} provided @{term "\ \ t = t"} holds for all permutations @{text "\"}. \end{definition} \noindent - We will be mainly interested in the case where @{text t} is a constant, but - of course there is no way to restrict this definition in Isabelle/HOL to just - this case. + We will primarily be interested in the cases where @{text t} is a constant, but + of course there is no way to restrict this definition in Isabelle/HOL so that it + applies to just constants. There are a number of equivalent formulations for the equivariance property. For example, assuming @{text t} is of permutation type @{text "\ \ @@ -533,15 +535,17 @@ \end{isabelle} \noindent + We will call this formulation of equivariance in \emph{fully applied form}. To see that this formulation implies the definition, we just unfold the definition of the permutation operation for functions and simplify with the equation and the cancellation property shown in \eqref{cancel}. To see the other direction, we use \eqref{permutefunapp}. Similarly for HOL-terms that take more than - one argument. + one argument. The point to note is that equivariance and equivariance in fully + applied form are always interderivable. Both formulations of equivariance have their advantages and - disadvantages: \eqref{altequivariance} is usually easier to + disadvantages: \eqref{altequivariance} is usually more convenient to establish, since statements in Isabelle/HOL are commonly given in a form where functions are fully applied. For example we can easily show that equality is equivariant @@ -570,113 +574,139 @@ \noindent for all @{text a}, @{text b} and @{text \}. Also the booleans @{const True} and @{const False} are equivariant by the definition - of the permutation operation for booleans. It is also easy to see + of the permutation operation for booleans. It is easy to see that the boolean operators, like @{text "\"}, @{text "\"}, @{text - "\"} and @{text "\"} are all equivariant (see ??? intro) + "\"} and @{text "\"}, are all equivariant too. (see ??? intro) In contrast, the advantage of Definition \ref{equivariance} is that - it leads to a simple rewrite system that allows us to `push' a - permutation towards the leaves in a HOL-term (i.e.~constants and free - variables). The permutation disappears in cases where the - constants are equivariant. Given a database of equivariant constants, - we can implement a decision procedure that helps to find out when - a compound term is equivariant. A permutation @{text \} can be pushed into - applications and abstractions in a HOL-term as follows + it leads to a relatively simple rewrite system that allows us to `push' a permutation, + say @{text \}, towards the leaves of a HOL-term (i.e.~constants and + variables). Then the permutation disappears in cases where the + constants are equivariant, since by Definition \ref{equivariance} we + have @{term "\ \ c = c"}. What we will show next is that for a HOL-term + @{term t} containing only equivariant constants, a permutation can be pushed + inside this term and the only instances remaining are in front of + the free variables of @{text t}. We can only show this by a meta-argument, + that means one we cannot formalise inside Isabelle/HOL. But we can invoke + it in form of a tactic programmed on the ML-level of Isabelle/HOL. + This tactic is a rewrite systems consisting of `oriented' equations. + + A permutation @{text \} can be + pushed into applications and abstractions as follows \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}lrcl} - i) & @{text "\ \ (t\<^isub>1 t\<^isub>2)"} & @{text "\"} & @{term "(\ \ t\<^isub>1) (\ \ t\<^isub>2)"}\\ - ii) & @{text "\ \ (\x. t)"} & @{text "\"} & @{text "\x. \ \ (t[x := (-\) \ x])"}\\ + i) & @{text "\ \ (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ + & @{term "(\ \ t\<^isub>1) (\ \ t\<^isub>2)"}\\ + ii) & @{text "\ \ (\x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\x. \ \ (t[x := (-\) \ x])"}\\ \end{tabular}\hfill\numbered{rewriteapplam} \end{isabelle} \noindent - The first rewrite rule we established as equation in \eqref{permutefunapp}; + The first rule we established in \eqref{permutefunapp}; the second follows from the definition of permutations acting on functions - and the fact that HOL-terms are considered equal modulo beta-reduction. - The inverse permutations that are introduced by the second rewrite rule - can be removed using the additional rewrite rule + and the fact that HOL-terms are equal modulo beta-equivalence. + Once the permutations are pushed towards the leaves we need the + following two rules \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}rcl} - @{term "\ \ (- \) \ x"} & @{text "\"} & @{term "x"} - \end{tabular}\hfill\numbered{rewriteunpermute} + \begin{tabular}{@ {}lrcl} + iii) & @{term "\ \ (- \) \ x"} & $\stackrel{\rightharpoonup}{=}$ & @{term "x"}\\ + iv) & @{term "\ \ c"} & $\stackrel{\rightharpoonup}{=}$ & + @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\ + \end{tabular}\hfill\numbered{rewriteother} \end{isabelle} \noindent - and permutations in front of equivariant constants can be removed by the - rule + in order to remove permuations in front of bound variables and equivariant constants. + + In order to obtain a terminating rewrite system, we have to be + careful with rule ({\it i}). It can lead to a loop whenever + \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "\' \ t'"}. Consider + for example the infinite reduction sequence \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}rcl} - @{term "\ \ c"} & @{text "\"} & @{term "c"} - \end{tabular}\hfill\numbered{rewriteconsts} + \begin{tabular}{@ {}l} + @{text "\ \ (\' \ t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\ + @{text "(\ \ \') \ (\ \ t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\ + @{text "((\ \ \') \ \) \ ((\ \ \') \ t)"}~~$\stackrel{\rightharpoonup}{=}\ldots$\\ + \end{tabular} \end{isabelle} - \noindent - By a meta-argument, that means one we cannot formalise inside - Isabelle/HOL, we can convince ourselves that the strategy of - of first pushing a permutation inside a term using - \eqref{rewriteapplam}, then removing permutation in front of bound - variables using \eqref{rewriteunpermute} and finally removing all - permutations in front of equivariant constants must terminate: the - size of the term gets smaller in \eqref{rewriteapplam} if we do not - count the inverse permutations introduced by the second rewrite rule - and there can only be finitely many bound variables in a term - (similarly equivariant constants), therefore only finitely many - applications of \eqref{rewriteunpermute} and - \eqref{rewriteconsts}. The only problem is that instances where - rules (\ref{rewriteapplam}.{\it i}) or rules - \eqref{rewriteunpermute} apply `overlap' and potentially our measure - increases. Consider for example the term @{term "\ \ (\x. x)"}, - whose final reduct should just be \mbox{@{term "\x. x"}}. Using - (\ref{rewriteapplam}.{\it ii}), the term can reduce to @{term - "\x. \ \ (- \) \ x"}, to which we can apply \eqref{rewriteunpermute} - in order to obtain the desired result. However, the subterm term @{text "(- - \) \ x"} is also an application (in fact three nested ones). Therefore - @{term "\x. \ \ (- \) \ x"} can also rewrite - to @{text "\x. (- (\ \ \)) \ (\ \ x)"} to which we cannot apply - (\ref{rewriteapplam}.{\it i}) directly and even worse our measure - increased. In order to distinguish situations where \eqref{rewriteconsts} - should apply instead of (\ref{rewriteapplam}.{\it i}) we use a standard - trick in HOL. We introduce a separate definition for terms of the form - @{text "(- \) \ x"}, namely as + where the last step is again an instance of the first term, but it is + bigger (note that for the permutation operation we have that @{text + "\ \ (op \) = (op \)"} since as shown in Lemma \ref{permutecompose} + \mbox{@{text "(op \)"}} is equivariant). In order to avoid this loop + we need to apply these rules using an `outside to inside' strategy. + This strategy is sufficient since we are only interested of rewriting + terms of the form @{term "\ \ t"}. + + Another problem we have to avoid is that the rules ({\it i}) and + ({\it iii}) can `overlap'. For this note that + the term @{term "\ \(\x. x)"} reduces to @{term "\x. \ \ (- \) \ + x"}, to which we can apply rule ({\it iii}) in order to obtain + @{term "\x. x"}, as is desired. However, the subterm term @{text + "(- \) \ x"} is also an application. Consequently, the term + @{term "\x. \ \ (- \) \x"} can reduce to @{text "\x. (- (\ \ \)) \ (\ \ x)"} using + ({\it i}). Now we cannot apply rule ({\it iii}) anymore and even + worse the measure we will introduce shortly increases. On the + other hand, if we started with the term @{text "\ \ ((- \) \ x)"} + where @{text \} and @{text x} are free variables, then we do + want to apply rule ({\it i}), rather than rule ({\it iii}) which + would eliminate @{text \} completely. This is a problem because we + want to keep the shape of the HOL-term intact during rewriting. + As a remedy we use a standard trick in HOL: we introduce + a separate definition for terms of the form @{text "(- \) \ x"}, + namely as \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @{term "unpermute \ x \ (- \) \ x"} \end{isabelle} \noindent - With this trick, we can reformulate our rewrite rules pushing a permutation @{text \} - inside a term as follows + The point is that we will always start with a term that does not + contain any @{text unpermutes}. With this trick we can reformulate + our rewrite rules as follows \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}lrcl} - i) & @{text "\ \ (t\<^isub>1 t\<^isub>2)"} & @{text "\"} & @{term "(\ \ t\<^isub>1) (\ \ t\<^isub>2)"}\hspace{45mm}\mbox{}\\ + i') & @{text "\ \ (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ & + @{term "(\ \ t\<^isub>1) (\ \ t\<^isub>2)"}\hspace{45mm}\mbox{}\\ \multicolumn{4}{r}{provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \ x"}}\smallskip\\ - ii) & @{text "\ \ (\x. t)"} & @{text "\"} & @{text "\x. \ \ (t[x := unpermute \ x])"}\\ - iii) & @{text "\ \ (unpermute \ x)"} & @{text "\"} & @{term x}\\ - iv) & @{term "\ \ c"} & @{text "\"} & @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\ + ii') & @{text "\ \ (\x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\x. \ \ (t[x := unpermute \ x])"}\\ + iii') & @{text "\ \ (unpermute \ x)"} & $\stackrel{\rightharpoonup}{=}$ & @{term x}\\ + iv') & @{term "\ \ c"} & $\stackrel{\rightharpoonup}{=}$ & @{term "c"} + \hspace{6mm}provided @{text c} is equivariant\\ \end{tabular} \end{isabelle} \noindent - In this rewrite systems no rule overlaps. Taking the measure + None of these rules overlap. To see that the permutation on the + right-hand side is applied to a smaller term, we take the measure consisting of lexicographically ordered pairs whose first component - is the size of the term (without counting @{text unpermutes}) and - the second is the number of occurences of @{text "unpermute \ x"} - and @{text "\ \ c"}, then each rule is strictly decreasing. - Consequently the process of applying these rules must terminate. - + is the size of a term (without counting @{text unpermutes}) and the + second is the number of occurences of @{text "unpermute \ x"} and + @{text "\ \ c"}. This means the process of applying these rules + with our `outside-to-inside' strategy must terminate. - together with the permutation - operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel} - leads to a simple rewrite system that pushes permutations inside a term until they reach - either function constants or variables. The permutations in front of - equivariant constants disappear. This helps us to establish equivariance - for any notion in HOL that is defined in terms of more primitive notions. To - see this let us + With the rewriting system in plcae, we are able to establish the + fact that for a HOL-term @{text t} whose constants are all equivariant, + the HOL-term @{text "\ \ t"} is equal to @{text "t'"} wherby + @{text "t'"} is equal to @{text t} except that every free variable + @{text x} of @{text t} is replaced by @{text "\ \ x"}. Pitts calls + this fact \emph{equivariance principle}. In our setting the precise + statement of this fact is a bit more involved because of the fact + that @{text unpermute} needs to be treated specially. + + \begin{theorem}[Equivariance Principle] + Suppose a HOL-term @{text t} does not contain any @{text unpermutes} and all + its constants are equivariant. For any permutation @{text \}, let @{text t'} + be the HOL-term @{text t} except every free variable @{text x} in @{term t} is + replaced by @{text "\ \ x"}, then @{text "\ \ t = t'"}. + \end{theorem} + + With these definitions in place we can define the notion of an \emph{equivariant} HOL-term @@ -714,6 +744,10 @@ Such a rewrite system is often very helpful in determining whether @{text "\ \ t = t"} holds for a compound term @{text t}. ??? + For this we have implemented in Isabelle/HOL a + database of equivariant constants that can be used to rewrite + HOL-terms. + *}