21 \begin{center} |
21 \begin{center} |
22 $t ::= x \mid t\;t \mid \lambda x. t$ |
22 $t ::= x \mid t\;t \mid \lambda x. t$ |
23 \end{center} |
23 \end{center} |
24 |
24 |
25 \noindent |
25 \noindent |
|
26 where bound variables have a name. |
26 For such terms it derives automatically a reasoning |
27 For such terms it derives automatically a reasoning |
27 infrastructure, which has been used in formalisations of an equivalence |
28 infrastructure, which has been used in formalisations of an equivalence |
28 checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
29 checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
29 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
30 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
30 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result |
31 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result |
146 \begin{center} |
147 \begin{center} |
147 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ |
148 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ |
148 \end{center} |
149 \end{center} |
149 |
150 |
150 \noindent |
151 \noindent |
151 where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound |
152 where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes |
152 in $s$. In this representation we need additional predicates to ensure |
153 bound in $s$. In this representation we need additional predicates to ensure |
153 that the two lists are of equal length. This can result into very |
154 that the two lists are of equal length. This can result into very |
154 unintelligible reasoning (see for example~\cite{BengtsonParow09}). |
155 unintelligible reasoning (see for example~\cite{BengtsonParow09}). |
155 |
156 To avoid this, we will allow for example specifications of $\mathtt{let}$s |
156 |
157 as follows |
157 |
158 |
158 |
159 \begin{center} |
159 |
160 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
|
161 $trm$ & $::=$ & \ldots\\ |
|
162 & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;t\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN t$\\[1mm] |
|
163 $assn$ & $::=$ & $\mathtt{anil}$\\ |
|
164 & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$ |
|
165 \end{tabular} |
|
166 \end{center} |
|
167 |
|
168 \noindent |
|
169 where $assn$ is an auxiliary type representing a list of assignments |
|
170 and $bn$ an auxilary function identifying the variables to be bound by |
|
171 the $\mathtt{let}$, given by |
|
172 |
|
173 \begin{center} |
|
174 $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ |
|
175 \end{center} |
|
176 |
|
177 \noindent |
|
178 This style of specifications for term-calculi with multiple binders is heavily |
|
179 inspired by the Ott-tool \cite{ott-jfp}. |
|
180 |
|
181 We will not be able to deal with all specifications that are allowed by |
|
182 Ott. One reason is that we establish the reasoning infrastructure for |
|
183 alpha-\emph{equated} terms. In contrast, Ott produces for a subset of its |
|
184 specifiactions a reasoning infrastructure involving concrete, |
|
185 \emph{non}-alpha-equated terms. To see the difference, note that working |
|
186 with alpha-equated terms means that the two type-schemes with $x$, $y$ and |
|
187 $z$ being distinct |
|
188 |
|
189 \begin{center} |
|
190 $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ |
|
191 \end{center} |
|
192 |
|
193 \noindent |
|
194 are not just alpha-equal, but actually equal---we are working with |
|
195 alpha-equivalence classes, but still have that bound variables |
|
196 carry a name. |
|
197 Our insistence on reasoning with alpha-equated terms comes from the |
|
198 wealth of experience we gained with the older version of Nominal |
|
199 Isabelle: for non-trivial properties, |
|
200 reasoning about alpha-equated terms is much easier than reasoning |
|
201 with concrete terms. The fundamental reason is that the HOL-logic |
|
202 underlying Nominal Isabelle allows us to replace ``equals-by-equals''. |
|
203 Replacing ``alpha-equals-by-alpha-equals'' requires a lot of work. |
|
204 |
|
205 Although a reasoning infrastructure for alpha-equated terms with names |
|
206 is in informal reasoning nearly always taken for granted, establishing |
|
207 it automatically in a theorem prover is a rather non-trivial task. |
|
208 For every specification we will construct a type that contains |
|
209 exactly the corresponding alpha-equated terms. For this we use the |
|
210 standard HOL-technique of defining a new type that has been |
|
211 identified as a non-empty subset of an existing type. In our |
|
212 context we take as the starting point the type of sets of concrete |
|
213 terms (the latter being defined as datatypes). Then quotient these |
|
214 sets according to our alpha-equivalence relation and then identifying |
|
215 the new type as these alpha-equivalence classes. The construction we |
|
216 can perform in HOL is illustrated by the following picture: |
|
217 |
|
218 |
|
219 |
160 Contributions: We provide definitions for when terms |
220 Contributions: We provide definitions for when terms |
161 involving general bindings are alpha-equivelent. |
221 involving general bindings are alpha-equivelent. |
162 |
222 |
163 %\begin{center} |
223 \begin{center} |
|
224 figure |
164 %\begin{pspicture}(0.5,0.0)(8,2.5) |
225 %\begin{pspicture}(0.5,0.0)(8,2.5) |
165 %%\showgrid |
226 %%\showgrid |
166 %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) |
227 %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5) |
167 %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} |
228 %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6} |
168 %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9) |
229 %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9) |
178 %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}} |
239 %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}} |
179 %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}} |
240 %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}} |
180 %\rput[c](1.7,1.5){$\lama$} |
241 %\rput[c](1.7,1.5){$\lama$} |
181 %\rput(3.7,1.75){isomorphism} |
242 %\rput(3.7,1.75){isomorphism} |
182 %\end{pspicture} |
243 %\end{pspicture} |
183 %\end{center} |
244 \end{center} |
184 |
245 |
185 quotient package \cite{Homeier05} |
246 \noindent |
|
247 To ``lift'' the reasoning from the underlying type to the new type |
|
248 is usually a tricky task. To ease this task we reimplemented in Isabelle/HOL |
|
249 the quotient package described by Homeier in \cite{Homeier05}. This |
|
250 re-implementation will automate the proofs we require for our |
|
251 reasoning infrastructure over alpha-equated terms.\medskip |
|
252 |
|
253 \noindent |
|
254 {\bf Contributions:} We provide new definitions for when terms |
|
255 involving multiple binders are alpha-equivalent. These definitions are |
|
256 inspired by earlier work of Pitts \cite{}. By means of automatic |
|
257 proofs, we establish a reasoning infrastructure for alpha-equated |
|
258 terms, including properties about support, freshness and equality |
|
259 conditions for alpha-equated terms. We will also derive for these |
|
260 terms a strong induction principle that has the variable convention |
|
261 already built in. |
186 *} |
262 *} |
187 |
263 |
188 section {* A Short Review of the Nominal Logic Work *} |
264 section {* A Short Review of the Nominal Logic Work *} |
189 |
265 |
190 text {* |
266 text {* |