42 (*>*) |
42 (*>*) |
43 |
43 |
44 section {* Introduction *} |
44 section {* Introduction *} |
45 |
45 |
46 text {* |
46 text {* |
47 The purpose of Nominal Isabelle is to provide a proving infratructure |
47 Nominal Isabelle provides a proving infratructure for |
48 for conveninet reasoning about programming languages. At its core |
48 convenient reasoning about programming languages. At its core Nominal |
49 Nominal Isabelle is based on nominal logic by Pitts at al |
49 Isabelle is based on the nominal logic work by Pitts at al |
50 \cite{GabbayPitts02,Pitts03}. |
50 \cite{GabbayPitts02,Pitts03}. The most basic notion in this work |
51 |
51 is a sort-respecting permutation operation defined over a countably infinite |
52 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
52 collection of sorted atoms. The atoms are used for representing variables |
53 prover providing a proving infrastructure for convenient reasoning about |
53 that might be bound. Multiple sorts are necessary for being able to |
54 programming languages. At its core Nominal Isabelle is based on the nominal |
54 represent different kinds of variables. For example, in the language Mini-ML |
55 logic work of Pitts et al \cite{GabbayPitts02,Pitts03}. The most basic |
55 there are bound term variables and bound type variables; each kind needs to |
56 notion in this work is a sort-respecting permutation operation defined over |
56 be represented by a different sort of atoms. |
57 a countably infinite collection of sorted atoms. The atoms are used for |
|
58 representing variables that might be bound. Multiple sorts are necessary for |
|
59 being able to represent different kinds of variables. For example, in the |
|
60 language Mini-ML there are bound term variables and bound type variables; |
|
61 each kind needs to be represented by a different sort of atoms. |
|
62 |
|
63 |
57 |
64 Unfortunately, the type system of Isabelle/HOL is not a good fit for the way |
58 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. |
59 atoms and sorts are used in the original formulation of the nominal logic work. |
66 Therefore it was decided in earlier versions of Nominal Isabelle to use a |
60 The reason is that one has to ensure that permutations are sort-respecting. |
67 separate type for each sort of atoms and let the type system enforce the |
61 This was done implicitly in the original nominal logic work \cite{Pitts03}. |
68 sort-respecting property of permutations. Inspired by the work on nominal |
62 |
69 unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also |
63 |
70 implement permutations concretely as lists of pairs of atoms. Thus Nominal |
|
71 Isabelle used the two-place permutation operation with the generic type |
64 Isabelle used the two-place permutation operation with the generic type |
72 |
65 |
73 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
66 @{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
74 |
67 |
75 \noindent |
68 \noindent |
222 The novel |
215 The novel |
223 technical contribution is a mechanism for dealing with |
216 technical contribution is a mechanism for dealing with |
224 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
217 ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages |
225 \cite{PittsHOL4} where variables and variable binding depend on type |
218 \cite{PittsHOL4} where variables and variable binding depend on type |
226 annotations. |
219 annotations. |
|
220 |
|
221 Therefore it was decided in earlier versions of Nominal Isabelle to use a |
|
222 separate type for each sort of atoms and let the type system enforce the |
|
223 sort-respecting property of permutations. Inspired by the work on nominal |
|
224 unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also |
|
225 implement permutations concretely as lists of pairs of atoms. |
|
226 |
227 |
227 |
228 *} |
228 *} |
229 |
229 |
230 section {* Sorted Atoms and Sort-Respecting Permutations *} |
230 section {* Sorted Atoms and Sort-Respecting Permutations *} |
231 |
231 |