49 %\rput[c](1.7,1.5){$\lama$} |
49 %\rput[c](1.7,1.5){$\lama$} |
50 %\rput(3.7,1.75){isomorphism} |
50 %\rput(3.7,1.75){isomorphism} |
51 %\end{pspicture} |
51 %\end{pspicture} |
52 %\end{center} |
52 %\end{center} |
53 |
53 |
54 |
54 quotient package \cite{Homeier05} |
55 *} |
55 *} |
56 |
56 |
57 section {* A Short Review of the Nominal Logic Work *} |
57 section {* A Short Review of the Nominal Logic Work *} |
58 |
58 |
59 text {* |
59 text {* |
60 At its core, Nominal Isabelle is based on the nominal logic work by Pitts |
60 At its core, Nominal Isabelle is based on the nominal logic work by Pitts |
61 \cite{Pitts03}. Two central notions in this work are sorted atoms and |
61 \cite{Pitts03}. The implementation of this work are described in |
62 permutations of atoms. The sorted atoms represent different |
62 \cite{HuffmanUrban10}, which we review here briefly to aid the description |
63 kinds of variables, such as term- and type-variables in Core-Haskell, and it |
63 of what follows in the next sections. Two central notions in the nominal |
64 is assumed that there is an infinite supply of atoms for each sort. |
64 logic work are sorted atoms and permutations of atoms. The sorted atoms |
65 However, in order to simplify the description of our work, we shall |
65 represent different kinds of variables, such as term- and type-variables in |
66 assume in this paper that there is only a single sort of atoms. |
66 Core-Haskell, and it is assumed that there is an infinite supply of atoms |
|
67 for each sort. However, in order to simplify the description of our work, we |
|
68 shall assume in this paper that there is only a single sort of atoms. |
67 |
69 |
68 Permutations are bijective functions from atoms to atoms that are |
70 Permutations are bijective functions from atoms to atoms that are |
69 the identity everywhere except on a finite number of atoms. There is a |
71 the identity everywhere except on a finite number of atoms. There is a |
70 two-place permutation operation written |
72 two-place permutation operation written |
71 |
73 |
94 for an @{text x}, defined as |
96 for an @{text x}, defined as |
95 |
97 |
96 @{thm[display,indent=5] fresh_def[no_vars]} |
98 @{thm[display,indent=5] fresh_def[no_vars]} |
97 |
99 |
98 \noindent |
100 \noindent |
99 We also use for sets of atoms the abbreviation @{thm fresh_star_def[no_vars]}. |
101 We also use for sets of atoms the abbreviation |
|
102 @{thm (lhs) fresh_star_def[no_vars]} defined as |
|
103 @{thm (rhs) fresh_star_def[no_vars]}. |
100 A striking consequence of these definitions is that we can prove |
104 A striking consequence of these definitions is that we can prove |
101 without knowing anything about the structure of @{term x} that |
105 without knowing anything about the structure of @{term x} that |
102 swapping two fresh atoms, say @{text a} and @{text b}, leave |
106 swapping two fresh atoms, say @{text a} and @{text b}, leave |
103 @{text x} unchanged. |
107 @{text x} unchanged. |
104 |
108 |
105 \begin{Property} |
109 \begin{property} |
106 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
110 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
107 \end{Property} |
111 \end{property} |
108 |
112 |
109 \begin{Property} |
113 \noindent |
|
114 For a proof see \cite{HuffmanUrban10}. |
|
115 |
|
116 \begin{property} |
110 @{thm[mode=IfThen] at_set_avoiding[no_vars]} |
117 @{thm[mode=IfThen] at_set_avoiding[no_vars]} |
111 \end{Property} |
118 \end{property} |
112 |
119 |
113 *} |
120 *} |
114 |
121 |
115 |
122 |
116 section {* Abstractions *} |
123 section {* Abstractions *} |
117 |
124 |
|
125 text {* |
|
126 General notion of alpha-equivalence (depends on a free-variable |
|
127 function and a relation). |
|
128 *} |
|
129 |
118 section {* Alpha-Equivalence and Free Variables *} |
130 section {* Alpha-Equivalence and Free Variables *} |
119 |
131 |
120 section {* Examples *} |
132 section {* Examples *} |
|
133 |
|
134 section {* Adequacy *} |
|
135 |
|
136 section {* Related Work *} |
121 |
137 |
122 section {* Conclusion *} |
138 section {* Conclusion *} |
123 |
139 |
124 text {* |
140 text {* |
125 |
141 |
|
142 TODO: function definitions: |
|
143 \medskip |
|
144 |
126 \noindent |
145 \noindent |
127 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the |
146 {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the |
128 many discussions about Nominal Isabelle. We thank Peter Sewell for |
147 many discussions about Nominal Isabelle. We thank Peter Sewell for |
129 making the informal notes \cite{SewellBestiary} available to us and |
148 making the informal notes \cite{SewellBestiary} available to us and |
130 also explaining some of the finer points of the OTT-tool. |
149 also for explaining some of the finer points of the OTT-tool. |
131 |
150 |
132 |
151 |
133 *} |
152 *} |
134 |
153 |
135 |
154 |