--- 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 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\
+ @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\smallskip\\
@{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\
& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\
- & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"}
+ & @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"}\\
+ & @{text "\<equiv>"} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"}
\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 | \<lambda>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 "\<pi> \<bullet> t = t"} holds for all permutations @{text "\<pi>"}.
\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 "\<alpha> \<Rightarrow>
@@ -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 \<pi>}. 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 "\<and>"}, @{text "\<or>"}, @{text
- "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro)
+ "\<not>"} and @{text "\<longrightarrow>"}, 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 \<pi>} 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 \<pi>}, 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 "\<pi> \<bullet> 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 \<pi>} can be
+ pushed into applications and abstractions as follows
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}lrcl}
- i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
- ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\
+ i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$
+ & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
+ ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> 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 "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}
- \end{tabular}\hfill\numbered{rewriteunpermute}
+ \begin{tabular}{@ {}lrcl}
+ iii) & @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & $\stackrel{\rightharpoonup}{=}$ & @{term "x"}\\
+ iv) & @{term "\<pi> \<bullet> 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 "\<pi>' \<bullet> t'"}. Consider
+ for example the infinite reduction sequence
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}{@ {}rcl}
- @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}
- \end{tabular}\hfill\numbered{rewriteconsts}
+ \begin{tabular}{@ {}l}
+ @{text "\<pi> \<bullet> (\<pi>' \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\
+ @{text "(\<pi> \<bullet> \<pi>') \<bullet> (\<pi> \<bullet> t)"}~~$\stackrel{\rightharpoonup}{=}\ldots\stackrel{\rightharpoonup}{=}$\\
+ @{text "((\<pi> \<bullet> \<pi>') \<bullet> \<pi>) \<bullet> ((\<pi> \<bullet> \<pi>') \<bullet> 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 "\<pi> \<bullet> (\<lambda>x. x)"},
- whose final reduct should just be \mbox{@{term "\<lambda>x. x"}}. Using
- (\ref{rewriteapplam}.{\it ii}), the term can reduce to @{term
- "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply \eqref{rewriteunpermute}
- in order to obtain the desired result. However, the subterm term @{text "(-
- \<pi>) \<bullet> x"} is also an application (in fact three nested ones). Therefore
- @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"} can also rewrite
- to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> 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 "(- \<pi>) \<bullet> 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
+ "\<pi> \<bullet> (op \<bullet>) = (op \<bullet>)"} since as shown in Lemma \ref{permutecompose}
+ \mbox{@{text "(op \<bullet>)"}} 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 "\<pi> \<bullet> 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 "\<pi> \<bullet>(\<lambda>x. x)"} reduces to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>
+ x"}, to which we can apply rule ({\it iii}) in order to obtain
+ @{term "\<lambda>x. x"}, as is desired. However, the subterm term @{text
+ "(- \<pi>) \<bullet> x"} is also an application. Consequently, the term
+ @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> 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 "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"}
+ where @{text \<pi>} and @{text x} are free variables, then we do
+ want to apply rule ({\it i}), rather than rule ({\it iii}) which
+ would eliminate @{text \<pi>} 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 "(- \<pi>) \<bullet> x"},
+ namely as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"}
\end{isabelle}
\noindent
- With this trick, we can reformulate our rewrite rules pushing a permutation @{text \<pi>}
- 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 "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\
+ i') & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & $\stackrel{\rightharpoonup}{=}$ &
+ @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\
\multicolumn{4}{r}{provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\
- ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\
- iii) & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & @{text "\<longmapsto>"} & @{term x}\\
- iv) & @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\
+ ii') & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & $\stackrel{\rightharpoonup}{=}$ & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\
+ iii') & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & $\stackrel{\rightharpoonup}{=}$ & @{term x}\\
+ iv') & @{term "\<pi> \<bullet> 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 \<pi> x"}
- and @{text "\<pi> \<bullet> 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 \<pi> x"} and
+ @{text "\<pi> \<bullet> 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 "\<pi> \<bullet> 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 "\<pi> \<bullet> 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 \<pi>}, let @{text t'}
+ be the HOL-term @{text t} except every free variable @{text x} in @{term t} is
+ replaced by @{text "\<pi> \<bullet> x"}, then @{text "\<pi> \<bullet> 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 "\<pi> \<bullet> 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.
+
*}