--- a/Pearl-jv/Paper.thy Sat Apr 09 00:29:40 2011 +0100
+++ b/Pearl-jv/Paper.thy Sat Apr 09 13:44:49 2011 +0800
@@ -67,7 +67,11 @@
At its core Nominal Isabelle is based on the nominal logic work by
Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is
a sort-respecting permutation operation defined over a countably
- infinite collection of sorted atoms. The aim of this paper is to
+ infinite collection of sorted atoms.
+
+
+
+ The aim of this paper is to
describe how we adapted this work so that it can be implemented in a
theorem prover based on Higher-Order Logic (HOL). For this we
present the definition we made in the implementation and also review
@@ -314,11 +318,11 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
- @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
- @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
- @{thm group_add_class.left_minus[where a="\<pi>::perm"]}
- \end{tabular}
+ i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\
+ ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm}
+ iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm}
+ iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]}
+ \end{tabular}\hfill\numbered{grouplaws}
\end{isabelle}
\noindent
@@ -327,23 +331,28 @@
come in handy when we have to do calculations with permutations.
Note that Isabelle/HOL defies standard conventions of mathematical notation
by using additive syntax even for non-commutative groups. Obviously,
- composition of permutations is not commutative in general, because @{text
- "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the
+ composition of permutations is not commutative in general; for example
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "(a b) + (b c) \<noteq> (b c) + (a b)"}
+ \end{isabelle}
+
+ \noindent
+ But since the point of this paper is to implement the
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
the non-standard notation in order to reuse the existing libraries.
- A \emph{permutation operation}, written @{text "\<pi> \<bullet> x"}, applies a permutation
- @{text "\<pi>"} to an object @{text "x"} of type @{text \<beta>}, say.
- This operation has the type
+ A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"},
+ applies a permutation @{text "\<pi>"} to an object @{text "x"} of type
+ @{text \<beta>}, say. This operation has the type
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
\end{isabelle}
\noindent
- Isabelle/HOL will allow us to give a definition of this operation for
- `base' types, such as atoms, permutations, booleans and natural numbers,
- and for type-constructors, such as functions, sets, lists and products.
+ Isabelle/HOL allows us to give a definition of this operation for
+ `base' types, such as atoms, permutations, booleans and natural numbers:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
@@ -351,12 +360,20 @@
permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ \end{tabular}\hfill\numbered{permdefsbase}
+ \end{isabelle}
+
+ \noindent
+ and for type-constructors, such as functions, sets, lists and products:
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
& @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- \end{tabular}\hfill\numbered{permdefs}
+ \end{tabular}\hfill\numbered{permdefsconstrs}
\end{isabelle}
In order to reason abstractly about this operation,
@@ -371,8 +388,9 @@
\end{isabelle}
\noindent
- From these properties and the laws about groups follows that a
- permutation and its inverse cancel each other. That is
+ From these properties and the laws about groups
+ (\ref{grouplaws}.{\it iv }) follows that a permutation and its inverse
+ cancel each other. That is
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -447,16 +465,16 @@
and establish:
\begin{theorem}
- If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types,
- then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"},
- @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"},
- @{text bool} and @{text "nat"}.
+ The types @{type atom}, @{type perm}, @{type bool} and @{type nat}
+ are permutation types, and if @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text
+ "\<beta>\<^isub>2"} are permutation types, then so are \mbox{@{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}},
+ @{text "\<beta> set"}, @{text "\<beta> list"} and @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}.
\end{theorem}
\begin{proof}
All statements are by unfolding the definitions of the permutation
operations and simple calculations involving addition and
- minus. With permutations for example we have
+ minus. In case of permutations for example we have
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}[b]{@ {}rcl}
@@ -487,6 +505,8 @@
@{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.
An equivariant HOL-term is one that is invariant under the
permutation operation. This notion can be defined in Isabelle/HOL
@@ -498,6 +518,10 @@
\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.
+
There are a number of equivalent formulations for the equivariance
property. For example, assuming @{text t} is of permutation type @{text "\<alpha> \<Rightarrow>
\<beta>"}, then equivariance can also be stated as
@@ -530,12 +554,11 @@
\noindent
using the permutation operation on booleans and property
- \eqref{permuteequ}.
- Lemma~\ref{permutecompose} establishes that the
+ \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the
permutation operation is equivariant. The permutation operation for
- lists and products, shown in \eqref{permdefs}, state that the
+ lists and products, shown in \eqref{permdefsconstrs}, state that the
constructors for products, @{text "Nil"} and @{text Cons} are
- equivariant. Furthermore a simple calculation will show that our
+ equivariant. Furthermore a simple calculation will show that our
swapping functions are equivariant, that is
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -552,21 +575,102 @@
"\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro)
In contrast, the advantage of Definition \ref{equivariance} is that
- it leads to a simple rewrite system. Consider the following oriented
- versions
+ 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 over
+ applications and abstractions in a HOL-term 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])"}\\
+ \end{tabular}\hfill\numbered{rewriteapplam}
+ \end{isabelle}
+
+ \noindent
+ The first rewrite rule we established as equation 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
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}{@ {}rcl}
+ @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}
+ \end{tabular}\hfill\numbered{rewriteunpermute}
+ \end{isabelle}
+
+ \noindent
+ and permutations in front of equivariant constants can be removed by the
+ rule
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}rcl}
- @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\
- @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\
- @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}\\
- \end{tabular}\hfill\numbered{swapeqvt}
+ @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}
+ \end{tabular}\hfill\numbered{rewriteconsts}
\end{isabelle}
-
- of the equations
-together with the permutation
+ \noindent
+ By a meta-argument, that means one we cannot formalise inside
+ Isabelle/HOL, we can convince ourselves that the rewriting process
+ 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
+
+ \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
+
+ \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{}\\
+ \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\\
+ \end{tabular}
+ \end{isabelle}
+
+ \noindent
+ In this rewrite systems no rule overlaps. Taking 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.
+
+
+ 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
@@ -599,7 +703,7 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
& @{text "\<pi> \<bullet> (\<lambda>x. t)"}\\
- @{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefs}\\
+ @{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefsconstrs}\\
\end{tabular}\hfill\qed
\end{isabelle}