37 abbreviation |
37 abbreviation |
38 "sort_ty \<equiv> sort_of_ty" |
38 "sort_ty \<equiv> sort_of_ty" |
39 |
39 |
40 (*>*) |
40 (*>*) |
41 |
41 |
|
42 (* |
|
43 TODO: write about supp of finite sets, abstraction over finite sets |
|
44 *) |
|
45 |
42 section {* Introduction *} |
46 section {* Introduction *} |
43 |
47 |
44 text {* |
48 text {* |
45 TODO: write about supp of finite sets |
49 Nominal Isabelle provides a proving infratructure for convenient reasoning |
46 |
50 about programming languages involving binders such as lambda abstractions or |
47 Nominal Isabelle provides a proving infratructure for |
51 quantifications in type schemes: |
48 convenient reasoning about programming languages. At its core Nominal |
52 |
49 Isabelle is based on the nominal logic work by Pitts at al |
53 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
50 \cite{GabbayPitts02,Pitts03}. The most basic notion in this work |
54 @{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>,x\<^isub>n}. \<tau>"} |
51 is a sort-respecting permutation operation defined over a countably infinite |
55 \hfill\numbered{atomperm} |
52 collection of sorted atoms. The atoms are used for representing variables |
56 \end{isabelle} |
53 that might be bound. Multiple sorts are necessary for being able to |
57 |
|
58 \noindent |
|
59 At its core Nominal Isabelle is based on the nominal logic work by Pitts at |
|
60 al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a |
|
61 sort-respecting permutation operation defined over a countably infinite |
|
62 collection of sorted atoms. The atoms are used for representing variable names |
|
63 that might be free or bound. Multiple sorts are necessary for being able to |
54 represent different kinds of variables. For example, in the language Mini-ML |
64 represent different kinds of variables. For example, in the language Mini-ML |
55 there are bound term variables and bound type variables; each kind needs to |
65 there are bound term variables in lambda abstractions and bound type variables in |
56 be represented by a different sort of atoms. |
66 type schemes. In order to be able to separate them, each kind of variables needs to be |
|
67 represented by a different sort of atoms. |
57 |
68 |
58 In our formalisation of the nominal logic work, we have to make a design decision |
69 In our formalisation of the nominal logic work, we have to make a design decision |
59 about how to represent sorted atoms and sort-respecting permutations. One possibility |
70 about how to represent sorted atoms and sort-respecting permutations. One possibility |
60 is to |
71 is to have separate types for the different kinds of atoms. With this one can represent |
61 |
72 permutations as lists of pairs of atoms and the operation of applying |
62 |
73 a permutation to an object as the overloaded function |
63 |
|
64 % Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
|
65 % atoms and sorts are used in the original formulation of the nominal logic work. |
|
66 % The reason is that one has to ensure that permutations are sort-respecting. |
|
67 % This was done implicitly in the original nominal logic work \cite{Pitts03}. |
|
68 |
|
69 |
|
70 Isabelle used the two-place permutation operation with the generic type |
|
71 |
74 |
72 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
75 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
73 |
76 |
74 \noindent |
77 \noindent |
75 where @{text "\<alpha>"} stands for the type of atoms and @{text "\<beta>"} for the type |
78 where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type |
76 of the objects on which the permutation acts. For atoms of type @{text "\<alpha>"} |
79 of the objects on which the permutation acts. For atoms |
77 the permutation operation is defined over the length of lists as follows |
80 the permutation operation is defined over the length of lists as follows |
78 |
81 |
79 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
82 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
80 \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
83 \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
81 @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\ |
84 @{text "[] \<bullet> c"} & @{text "="} & @{text c}\\ |
89 \noindent |
92 \noindent |
90 where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and |
93 where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and |
91 @{text "b"}. For atoms of different type, the permutation operation |
94 @{text "b"}. For atoms of different type, the permutation operation |
92 is defined as @{text "\<pi> \<bullet> c \<equiv> c"}. |
95 is defined as @{text "\<pi> \<bullet> c \<equiv> c"}. |
93 |
96 |
94 With the list representation of permutations it is impossible to state an |
97 |
95 ``ill-sorted'' permutation, since the type system excludes lists containing |
98 % Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
96 atoms of different type. Another advantage of the list representation is that |
99 % atoms and sorts are used in the original formulation of the nominal logic work. |
97 the basic operations on permutations are already defined in the list library: |
100 % The reason is that one has to ensure that permutations are sort-respecting. |
98 composition of two permutations (written @{text "_ @ _"}) is just list append, |
101 % This was done implicitly in the original nominal logic work \cite{Pitts03}. |
99 and inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just |
102 |
100 list reversal. A disadvantage is that permutations do not have unique |
103 |
101 representations as lists; we had to explicitly identify permutations according |
104 With the separate atom types and the list representation of permutations it |
102 to the relation |
105 is impossible to state an ``ill-sorted'' permutation, since the type system |
|
106 excludes lists containing atoms of different type. However, whenever we |
|
107 need to generalise induction hypotheses by quantifying over permutations, we |
|
108 have to build cumbersome quantifications like |
|
109 |
|
110 @{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"} |
|
111 |
|
112 \noindent |
|
113 where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. |
|
114 The reason is that the permutation operation behaves differently for |
|
115 every @{text "\<alpha>\<^isub>i"}. Similarly, the notion of support |
|
116 |
|
117 @{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"} |
|
118 |
|
119 \noindent |
|
120 which we will define later, cannot be |
|
121 used to express the support of an object over \emph{all} atoms. The reason |
|
122 is that support can behave differently for each @{text |
|
123 "\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in |
|
124 a statement that an object, say @{text "x"}, is finitely supported we end up |
|
125 with having to state premises of the form |
|
126 |
|
127 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
128 \begin{tabular}{@ {}l} |
|
129 @{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"} |
|
130 \end{tabular}\hfill\numbered{fssequence} |
|
131 \end{isabelle} |
|
132 |
|
133 |
|
134 |
|
135 |
|
136 |
|
137 |
|
138 |
|
139 |
|
140 |
|
141 An advantage of the |
|
142 list representation is that the basic operations on permutations are already |
|
143 defined in the list library: composition of two permutations (written @{text |
|
144 "_ @ _"}) is just list append, and inversion of a permutation (written |
|
145 @{text "_\<^sup>-\<^sup>1"}) is just list reversal. A disadvantage is that |
|
146 permutations do not have unique representations as lists; we had to |
|
147 explicitly identify permutations according to the relation |
|
148 |
103 |
149 |
104 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
150 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
105 \begin{tabular}{@ {}l} |
151 \begin{tabular}{@ {}l} |
106 @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"} |
152 @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"} |
107 \end{tabular}\hfill\numbered{permequ} |
153 \end{tabular}\hfill\numbered{permequ} |