--- a/Pearl-jv/Paper.thy Mon Mar 14 16:35:59 2011 +0100
+++ b/Pearl-jv/Paper.thy Tue Mar 15 00:40:39 2011 +0100
@@ -90,8 +90,7 @@
by applying the inverse permutation. A corresponding inverse substitution
might not always exist, since renaming substitutions are in general only injective.
Another reason is that permutations preserve many constructions when reasoning about syntax.
- For example the validity of a typing context is preserved under any permutation.
- Suppose a typing context @{text "\<Gamma>"} of the form
+ For example, suppose a typing context @{text "\<Gamma>"} of the form
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"}
@@ -99,9 +98,9 @@
\noindent
is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"}
- occur twice. Then validity is preserved under
- permutations in the sense that if @{text \<Gamma>} is valid then so is @{text "\<pi> \<bullet> \<Gamma>"} for
- all permutations @{text "\<pi>"}. This is again \emph{not} the case for arbitrary
+ occur twice. Then validity of typing contexts is preserved under
+ permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for
+ all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary
renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}.
Permutations also behave uniformly with respect to HOL's logic connectives.
@@ -118,9 +117,9 @@
This uniform behaviour can also be extended to quantifiers and functions.
Because of these good properties of permutations, we are able to automate
reasoning to do with \emph{equivariance}. By equivariance we mean the property
- that every permutation leaves an object unchanged, that is @{term "\<pi> \<bullet> x = x"}
+ that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"}
for all @{text "\<pi>"}. This will often simplify arguments involving support
- and functions, since equivariant objects have empty support---or
+ of functions, since if they are equivariant then they have empty support---or
`no free atoms'.
There are a number of subtle differences between the nominal logic work by
@@ -158,7 +157,7 @@
text {*
The two most basic notions in the nominal logic work are a countably
- infinite collection of sorted atoms and sort-respecting permutations.
+ infinite collection of sorted atoms and sort-respecting permutations of atoms.
The existing nominal logic work usually leaves implicit
the sorting information for atoms and as far as we know leaves out a
description of how sorts are represented. In our formalisation, we
@@ -182,8 +181,8 @@
for their variables.} The use of type \emph{string} for sorts is merely for
convenience; any countably infinite type would work as well.
The set of all atoms we shall write as @{term "UNIV::atom set"}.
- We have two
- auxiliary functions @{text sort} and @{const nat_of} that are defined as
+ We have two auxiliary functions for atoms, namely @{text sort}
+ and @{const nat_of} which are defined as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -236,7 +235,7 @@
consider what happens if a user states a swapping of atoms with different
sorts. The following definition\footnote{To increase legibility, we omit
here and in what follows the @{term Rep_perm} and @{term "Abs_perm"}
- wrappers that are needed in our implementation since we defined permutation
+ wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation
not to be the full function space, but only those functions of type @{typ
perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.}
@@ -317,8 +316,19 @@
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
the non-standard notation in order to reuse the existing libraries.
- In order to reason abstractly about permutations, we use Isabelle/HOL's
- type classes~\cite{Wenzel04} and state the following two
+
+ A permutation operation, written @{text "\<pi> \<bullet> x"}, applies a permutation
+ @{text "\<pi>"} to an object @{text "x"}. This operation has the generic type
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ \end{isabelle}
+
+ \noindent
+ and Isabelle/HOL will allow us to give a definition of this operation for
+ `base' types, such as booleans and atoms, and for type-constructors, such as
+ products and lists. In order to reason abstractly about this operation,
+ we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two
\emph{permutation properties}:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -331,9 +341,10 @@
\noindent
The use of type classes allows us to delegate much of the routine resoning involved in
determining whether these properties are satisfied to Isabelle/HOL's type system:
- we only have to establish that `base' types, such as @{text booleans} and
- @{text atoms}, satisfy them and that type-constructors, such as products and lists,
- preserve them. For this we define
+ we only have to establish that base types satisfy them and that type-constructors
+ preserve them. Isabelle/HOL will use this information and determine whether
+ an object @{text x} with a compound type satisfies the permutation properties.
+ For this we define the notion of a \emph{permutation type}:
\begin{definition}[Permutation type]
A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
@@ -368,7 +379,26 @@
\end{isabelle}
\noindent
- In order to lift the permutation operation to other types, we can define for:
+ We can also show that the following property holds for any permutation type.
+
+ \begin{lemma}\label{permutecompose}
+ Given @{term x} is of permutation type, then
+ @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
+ \end{lemma}
+
+ \begin{proof} The proof is as follows:
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
+ & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\
+ @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\
+ @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
+ @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
+ \end{tabular}\hfill\qed
+ \end{isabelle}
+ \end{proof}
+
+ \noindent
+ Next we define the permutation operation for some types:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}}
@@ -385,7 +415,7 @@
\end{isabelle}
\noindent
- and then establish:
+ and establish:
\begin{theorem}
If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types,
@@ -420,47 +450,29 @@
\noindent
which is a simple consequence of the definition and the cancellation property in \eqref{cancel}.
- We can also show that the following property holds for any permutation type.
-
- \begin{lemma}\label{permutecompose}
- Given @{term x} is of permutation type, then
- @{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}.
- \end{lemma}
-
- \begin{proof} The proof is as follows:
- \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- \begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l}
- & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\
- @{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by \eqref{cancel}\\
- @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\
- @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\
- \end{tabular}\hfill\qed
- \end{isabelle}
- \end{proof}
-
*}
section {* Equivariance *}
text {*
An important notion in the nominal logic work is \emph{equivariance}.
- An equivariant function is one that is invariant under
- permutations of atoms. This notion can be defined
- uniformly as follows:
+ An equivariant function is one that is invariant under the
+ permutation operation. This notion can be defined
+ uniformly for all constants in HOL as follows:
\begin{definition}[Equivariance]\label{equivariance}
- A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
+ A constant @{text c} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> c = c"}.
\end{definition}
\noindent
There are a number of equivalent formulations for the equivariance property.
- For example, assuming @{text f} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance
+ For example, assuming @{text c} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance
can also be stated as
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{text "\<forall>\<pi> x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+ @{text "\<forall>\<pi> x. \<pi> \<bullet> (c x) = c (\<pi> \<bullet> x)"}
\end{tabular}\hfill\numbered{altequivariance}
\end{isabelle}
@@ -484,8 +496,10 @@
\noindent
using the permutation operation on booleans and property \eqref{permuteequ}.
Lemma~\ref{permutecompose} establishes that the permutation operation is
- equivariant. It is also easy to see that the boolean operators, like
- @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. Furthermore
+ equivariant. The permutation operation for lists and products, shown in \eqref{permdefs},
+ state that the constructors for products, @{text "Nil"} and @{text Cons} are equivariant. Also
+ the booleans @{const True} and @{const False} are equivariant by the permutation
+ operation. Furthermore
a simple calculation will show that our swapping functions are equivariant, that is
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -495,13 +509,61 @@
\end{isabelle}
\noindent
- for all @{text a}, @{text b} and @{text \<pi>}.
+ for all @{text a}, @{text b} and @{text \<pi>}.
+ It is also easy to see that the boolean operators, like
+ @{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant.
+
+ In contrast, the equation in Definition~\ref{equivariance} 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 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"}
+ \hfill\numbered{holterms}
+ \end{isabelle}
+
+ \noindent
+ whereby @{text c} stands for constants. 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.
+ With these definitions in place we can define the notion of an \emph{equivariant}
+ HOL-term
- In contrast, Definition~\ref{equivariance} together with the permutation
- operation for functions and \eqref{permutefunapp} lead 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 functions disappear. Such a rewrite system is often very helpful
+ \begin{definition}[Equivariant HOL-term]
+ A HOL-term is \emph{equivariant}, provided it is closed and composed of applications,
+ abstractions and equivariant constants only.
+ \end{definition}
+
+ \noindent
+ For equivariant terms we have
+
+ \begin{lemma}
+ For an equivariant HOL-term @{text "t"}, @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}.
+ \end{lemma}
+
+ \begin{proof}
+ By induction on the grammar of HOL-terms. The case for variables cannot arise since
+ equivariant HOL-terms are closed. The case for constants is clear by Definition
+ \ref{equivariance}. The case for applications is also straightforward since by
+ \eqref{permutefunapp} we have @{term "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2) = (\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}.
+ For the case of abstractions we can reason as follows
+
+ \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}\\
+
+ \end{tabular}\hfill\qed
+ \end{isabelle}
+ \end{proof}
+
+ database of equivariant functions
+
+ Such a rewrite system is often very helpful
in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ???
*}
--- a/Pearl-jv/document/root.tex Mon Mar 14 16:35:59 2011 +0100
+++ b/Pearl-jv/document/root.tex Tue Mar 15 00:40:39 2011 +0100
@@ -38,9 +38,9 @@
binding based on the notions of atoms, permutations and support. The
engineering challenge is to smoothly adapt this theory to a theorem prover
environment, in our case Isabelle/HOL. For this we have to formulate the
-theory so that it is compatible with HOL, which the original formulation by
-Pitts is not. We achieve this by not requiring that every object in our
-discourse has finite support. We present a formalisation that is based on a
+theory so that it is compatible with Higher-Order Logic, which the original formulation by
+Pitts is not. We achieve this by not requiring that every construction has
+to have finite support. We present a formalisation that is based on a
unified atom type and that represents permutations by bijective functions from
atoms to atoms. Interestingly, we allow swappings, which are permutations
build from two atoms, to be ill-sorted. We also describe a formalisation of