--- a/Pearl-jv/Paper.thy Wed Mar 02 00:06:28 2011 +0000
+++ b/Pearl-jv/Paper.thy Tue Mar 08 09:07:27 2011 +0000
@@ -44,11 +44,10 @@
text {*
Nominal Isabelle provides a proving infratructure for convenient reasoning
- about programming language calculi involving binders, such as lambda abstractions or
- quantifications in type schemes:
+ about syntax involving binders, such as lambda terms or type schemes:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
- @{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"}
+ @{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"}
\hfill\numbered{atomperm}
\end{isabelle}
@@ -56,12 +55,59 @@
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 nominal logic work has been starting
- point for a number of formalisations, most notable Norrish \cite{norrish04}
- in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own
- work in Isabelle/HOL.
+ collection of sorted atoms. The atoms are used for representing variable names
+ that might be 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
+ represented by a different sort of atoms.
+
+ The nominal logic work has been the starting point for a number of proving
+ infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by
+ Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and teh work by Urban
+ and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very
+ general notion, called \emph{support}, for the `set of free variables, or
+ atoms' of an object that applies not just to lambda terms and type schemes,
+ but also to sets, products, lists and even functions. The notion of support
+ is derived from the permutation operation defined over atoms. This
+ permutation operation, written @{text "_ \<bullet> _"}, has proved to be very
+ convenient for reasoning about syntax, in comparison to, say, arbitrary
+ renaming substitutions of atoms. The reason is that permutations are
+ bijective renamings of atoms and thus they can be easily `undone'---namely
+ by applying the inverse permutation. A corresponding inverse substitution
+ might not exist in general, since renaming substitutions are only injective.
+ Permutations also preserve many constructions when reasoning about syntax.
+ For example validity of a typing context is preserved under permutations.
+ 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"}
+ \end{isabelle}
+
+ \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 \emph{not} the case for arbitrary
+ renaming substitutions, as they might identify some variables in @{text \<Gamma>}.
+ Permutations fit well with HOL's definitions. For example
+
+ Because
+ of the good properties of permutations, we will be able to automate reasoning
+ steps determining when a construction in HOL is
+ \emph{equivariant}. By equivariance we mean the property that every
+ permutation leaves an object unchanged, that is @{term "\<forall>\<pi>. \<pi> \<bullet> x = x"}.
+ This will often simplify arguments involving the notion of support.
+
+
+ There are a number of subtle differences between the nominal logic work by Pitts
+ and the one we will present in this paper. Nominal
+
+ In the nominal logic work, the `new quantifier' plays a prominent role.
+
+
+
Using a single atom type to represent atoms of different sorts and
representing permutations as functions are not new ideas; see
\cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution
@@ -74,34 +120,30 @@
depend on type annotations.
The paper is organised as follows\ldots
+
+
+ Two binders
*}
section {* Sorted Atoms and Sort-Respecting Permutations *}
text {*
- The most basic notion in this work is a
+ The two most basic notions in the nominal logic work are
sort-respecting permutation operation defined over a countably infinite
- collection of sorted atoms. The atoms are used for representing variable names
- that might be 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
- represented by a different sort of atoms.
-
-
+ collection of sorted 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 therefore have to make a
design decision about how to implement sorted atoms and sort-respecting
- permutations. One possibility, which we described in \cite{Urban08}, is to
- have separate types for the different
- kinds of atoms, say types @{text "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}.
+ permutations. One possibility, which we described in \cite{Urban08}, is to
+ have separate types for the different kinds of atoms, say types @{text
+ "\<alpha>\<^isub>1,\<dots>,\<alpha>\<^isub>n"}. However, this does not blend well with the
+ resoning infrastructure of type-classes in Isabelle/HOL (see Section ???
+ about related work). Therefore we use here a single unified atom type to
+ represent atoms of different sorts. A basic requirement is that there must
+ be a countably infinite number of atoms of each sort. This can be
+ implemented as the datatype
- In the nominal logic work of Pitts, binders and bound variables are
- 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. We implement these atoms as
*}
datatype atom\<iota> = Atom\<iota> string nat
@@ -110,13 +152,19 @@
\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 of 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}
+ for their variables.} The use of type \emph{string} for sorts is merely for
+ convenience; any countably infinite type would work as well. We have an
+ auxiliary function @{text sort} that is defined as
+
+ \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
+ @{thm sort_of.simps[no_vars, THEN eq_reflection]}
+ \end{isabelle}
+
+ \noindent
+ and we clearly have for every finite set @{text S}
of atoms and every sort @{text s} the property:
- \begin{proposition}\label{choosefresh}
+ \begin{proposition}\label{choosefresh}\mbox{}\\
@{text "For a finite set of atoms S, there exists an atom a such that
sort a = s and a \<notin> S"}.
\end{proposition}
@@ -174,8 +222,8 @@
the value of @{text "(a b)"} is unspecified. However, this looked like a
cumbersome solution, since sort-related side conditions would be required
everywhere, even to unfold the definition. It turned out to be more
- convenient to actually allow the user to state ``ill-sorted'' swappings but
- limit their ``damage'' by defaulting to the identity permutation in the
+ convenient to actually allow the user to state `ill-sorted' swappings but
+ limit their `damage' by defaulting to the identity permutation in the
ill-sorted case:
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -191,7 +239,7 @@
@{text a} and @{text b}, and sort respecting. Therefore it is
a function in @{typ perm}.
- One advantage of using functions instead of lists as a representation for
+ One advantage of using functions as a representation for
permutations is that for example the swappings
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -202,16 +250,17 @@
\end{isabelle}
\noindent
- are \emph{equal}. We do not have to use the equivalence relation shown
- in~\eqref{permequ} to identify them, as we would if they had been represented
- as lists of pairs. Another advantage of the function representation is that
- they form a (non-commutative) group provided we define
+ are \emph{equal}. Therfore we can use for permutations HOL's built-in
+ principle of `replacing equals by equals in any context'. Another advantage
+ of the function representation is that they form a (non-commutative) group
+ provided we define
+
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
- @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
- @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
+ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{5mm}
+ @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{5mm}
+ @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{5mm}
@{thm minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]}
\end{tabular}
\end{isabelle}
@@ -221,16 +270,15 @@
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{3mm}
- @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{3mm}
- @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{3mm}
+ @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]} \hspace{5mm}
+ @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{5mm}
+ @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{5mm}
@{thm group_add_class.left_minus[where a="\<pi>::perm"]}
\end{tabular}
\end{isabelle}
\noindent
- Again this is in contrast to the list-of-pairs representation which does not
- form a group. The technical importance of this fact is that we can rely on
+ The technical importance of this fact is that we can rely on
Isabelle/HOL's existing simplification infrastructure for groups, which will
come in handy when we have to do calculations with permutations.
Note that Isabelle/HOL defies standard conventions of mathematical notation
@@ -240,9 +288,8 @@
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
the non-standard notation in order to reuse the existing libraries.
- By formalising permutations abstractly as functions, and using a single type
- for all atoms, we can now restate the \emph{permutation properties} from
- \eqref{permprops} as just the two equations
+ In order to reason abstractly about permutations, we state the following two
+ \emph{permutation properties}
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}}
@@ -252,14 +299,11 @@
\end{isabelle}
\noindent
- in which the permutation operations are of type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} and so
- have only a single type parameter. Consequently, these properties are
- compatible with the one-parameter restriction of Isabelle/HOL's type classes.
- There is no need to introduce a separate type class instantiated for each
- sort, like in the old approach.
-
- The next notion allows us to establish generic lemmas involving the
- permutation operation.
+ We state these properties in terms of Isabelle/HOL's type class
+ mechanism \cite{}.
+ This allows us to delegate much of the resoning involved in
+ determining whether these properties are satisfied to the type system.
+ For this we define
\begin{definition}
A type @{text "\<beta>"} is a \emph{permutation type} if the permutation
@@ -268,7 +312,8 @@
\end{definition}
\noindent
- First, it follows from the laws governing
+ The type class also allows us to establish generic lemmas involving the
+ permutation operation. First, it follows from the laws governing
groups that a permutation and its inverse cancel each other. That is, for any
@{text "x"} of a permutation type:
@@ -281,6 +326,7 @@
\end{isabelle}
\noindent
+ ??? Proof
Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective,
which in turn implies the property
@@ -316,16 +362,16 @@
\begin{equation}\label{permdefs}
\mbox{
- \begin{tabular}{@ {}ll@ {\hspace{2mm}}l@ {}}
- 1) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
- 2) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
- 3) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
- 4) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 5) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 6) & lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ \begin{tabular}{@ {}ll@ {\hspace{4mm}}l@ {}}
+ a) & atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\
+ b) & functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\
+ c) & permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\
+ d) & sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ e) & booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ f) & 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]}\\
- 7) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
- 8) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ g) & products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\
+ h) & nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\
\end{tabular}}
\end{equation}