76 easily by iterating single binders. For example in case of type-schemes we do not |
76 easily by iterating single binders. For example in case of type-schemes we do not |
77 want to make a distinction about the order of the bound variables. Therefore |
77 want to make a distinction about the order of the bound variables. Therefore |
78 we would like to regard the following two type-schemes as alpha-equivalent |
78 we would like to regard the following two type-schemes as alpha-equivalent |
79 % |
79 % |
80 \begin{equation}\label{ex1} |
80 \begin{equation}\label{ex1} |
81 @{text "\<forall>{x,y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y,x}. y \<rightarrow> x"} |
81 @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"} |
82 \end{equation} |
82 \end{equation} |
83 |
83 |
84 \noindent |
84 \noindent |
85 but assuming that @{text x}, @{text y} and @{text z} are distinct variables, |
85 but assuming that @{text x}, @{text y} and @{text z} are distinct variables, |
86 the following two should \emph{not} be alpha-equivalent |
86 the following two should \emph{not} be alpha-equivalent |
87 % |
87 % |
88 \begin{equation}\label{ex2} |
88 \begin{equation}\label{ex2} |
89 @{text "\<forall>{x,y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"} |
89 @{text "\<forall>{x, y}. x \<rightarrow> y \<notapprox>\<^isub>\<alpha> \<forall>{z}. z \<rightarrow> z"} |
90 \end{equation} |
90 \end{equation} |
91 |
91 |
92 \noindent |
92 \noindent |
93 Moreover, we like to regard type-schemes as alpha-equivalent, if they differ |
93 Moreover, we like to regard type-schemes as alpha-equivalent, if they differ |
94 only on \emph{vacuous} binders, such as |
94 only on \emph{vacuous} binders, such as |
95 % |
95 % |
96 \begin{equation}\label{ex3} |
96 \begin{equation}\label{ex3} |
97 @{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x,z}. x \<rightarrow> y"} |
97 @{text "\<forall>{x}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{x, z}. x \<rightarrow> y"} |
98 \end{equation} |
98 \end{equation} |
99 |
99 |
100 \noindent |
100 \noindent |
101 where @{text z} does not occur freely in the type. In this paper we will |
101 where @{text z} does not occur freely in the type. In this paper we will |
102 give a general binding mechanism and associated notion of alpha-equivalence |
102 give a general binding mechanism and associated notion of alpha-equivalence |
168 \end{center} |
168 \end{center} |
169 |
169 |
170 \noindent |
170 \noindent |
171 where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"} |
171 where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"} |
172 become bound in @{text s}. In this representation the term |
172 become bound in @{text s}. In this representation the term |
173 \mbox{@{text "\<LET> [x].s [t\<^isub>1,t\<^isub>2]"}} would be a perfectly legal |
173 \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} would be a perfectly legal |
174 instance. To exclude such terms, additional predicates about well-formed |
174 instance. To exclude such terms, additional predicates about well-formed |
175 terms are needed in order to ensure that the two lists are of equal |
175 terms are needed in order to ensure that the two lists are of equal |
176 length. This can result into very messy reasoning (see for |
176 length. This can result into very messy reasoning (see for |
177 example~\cite{BengtsonParow09}). To avoid this, we will allow type |
177 example~\cite{BengtsonParow09}). To avoid this, we will allow type |
178 specifications for $\mathtt{let}$s as follows |
178 specifications for $\mathtt{let}$s as follows |
228 and the raw terms produced by Ott use names for bound variables, |
228 and the raw terms produced by Ott use names for bound variables, |
229 there is a key difference: working with alpha-equated terms means that the |
229 there is a key difference: working with alpha-equated terms means that the |
230 two type-schemes (with $x$, $y$ and $z$ being distinct) |
230 two type-schemes (with $x$, $y$ and $z$ being distinct) |
231 |
231 |
232 \begin{center} |
232 \begin{center} |
233 @{text "\<forall>{x}. x \<rightarrow> y = \<forall>{x,z}. x \<rightarrow> y"} |
233 @{text "\<forall>{x}. x \<rightarrow> y = \<forall>{x, z}. x \<rightarrow> y"} |
234 \end{center} |
234 \end{center} |
235 |
235 |
236 \noindent |
236 \noindent |
237 are not just alpha-equal, but actually \emph{equal}. As a result, we can |
237 are not just alpha-equal, but actually \emph{equal}. As a result, we can |
238 only support specifications that make sense on the level of alpha-equated |
238 only support specifications that make sense on the level of alpha-equated |
251 terms is nearly always taken for granted, establishing it automatically in |
251 terms is nearly always taken for granted, establishing it automatically in |
252 the Isabelle/HOL theorem prover is a rather non-trivial task. For every |
252 the Isabelle/HOL theorem prover is a rather non-trivial task. For every |
253 specification we will need to construct a type containing as elements the |
253 specification we will need to construct a type containing as elements the |
254 alpha-equated terms. To do so, we use the standard HOL-technique of defining |
254 alpha-equated terms. To do so, we use the standard HOL-technique of defining |
255 a new type by identifying a non-empty subset of an existing type. The |
255 a new type by identifying a non-empty subset of an existing type. The |
256 construction we perform in HOL can be illustrated by the following picture: |
256 construction we perform in Isabelle/HOL can be illustrated by the following picture: |
257 |
257 |
258 \begin{center} |
258 \begin{center} |
259 \begin{tikzpicture} |
259 \begin{tikzpicture} |
260 %\draw[step=2mm] (-4,-1) grid (4,1); |
260 %\draw[step=2mm] (-4,-1) grid (4,1); |
261 |
261 |
324 \noindent |
324 \noindent |
325 (Note that this means also the term-constructors for variables, applications |
325 (Note that this means also the term-constructors for variables, applications |
326 and lambda are lifted to the quotient level.) This construction, of course, |
326 and lambda are lifted to the quotient level.) This construction, of course, |
327 only works if alpha-equivalence is indeed an equivalence relation, and the lifted |
327 only works if alpha-equivalence is indeed an equivalence relation, and the lifted |
328 definitions and theorems are respectful w.r.t.~alpha-equivalence. Accordingly, we |
328 definitions and theorems are respectful w.r.t.~alpha-equivalence. Accordingly, we |
329 will not be able to lift a bound-variable function to alpha-equated terms |
329 will not be able to lift a bound-variable function, which can be defined for |
|
330 raw terms, to alpha-equated terms |
330 (since it does not respect alpha-equivalence). To sum up, every lifting of |
331 (since it does not respect alpha-equivalence). To sum up, every lifting of |
331 theorems to the quotient level needs proofs of some respectfulness |
332 theorems to the quotient level needs proofs of some respectfulness |
332 properties. In the paper we show that we are able to automate these |
333 properties. In the paper we show that we are able to automate these |
333 proofs and therefore can establish a reasoning infrastructure for |
334 proofs and therefore can establish a reasoning infrastructure for |
334 alpha-equated terms.\medskip |
335 alpha-equated terms. |
|
336 |
|
337 The examples we have in mind where our reasoning infrastructure will be |
|
338 immeasurably helpful is what is often referred to as Core-Haskell (see |
|
339 Figure~\ref{corehas}). There terms include patterns which include a list of |
|
340 type- and term- variables (the arguments of constructors) all of which are |
|
341 bound in case expressions. One difficulty is that each of these variables |
|
342 come with a kind or type annotation. Representing such binders with single |
|
343 binders and reasoning about them in a theorem prover would be a major pain. |
|
344 \medskip |
335 |
345 |
336 |
346 |
337 \noindent |
347 \noindent |
338 {\bf Contributions:} We provide new definitions for when terms |
348 {\bf Contributions:} We provide new definitions for when terms |
339 involving multiple binders are alpha-equivalent. These definitions are |
349 involving multiple binders are alpha-equivalent. These definitions are |
341 proofs, we establish a reasoning infrastructure for alpha-equated |
351 proofs, we establish a reasoning infrastructure for alpha-equated |
342 terms, including properties about support, freshness and equality |
352 terms, including properties about support, freshness and equality |
343 conditions for alpha-equated terms. We are also able to derive, at the moment |
353 conditions for alpha-equated terms. We are also able to derive, at the moment |
344 only manually, strong induction principles that |
354 only manually, strong induction principles that |
345 have the variable convention already built in. |
355 have the variable convention already built in. |
|
356 |
|
357 \begin{figure} |
|
358 |
|
359 \caption{Core Haskell.\label{corehas}} |
|
360 \end{figure} |
346 *} |
361 *} |
347 |
362 |
348 section {* A Short Review of the Nominal Logic Work *} |
363 section {* A Short Review of the Nominal Logic Work *} |
349 |
364 |
350 text {* |
365 text {* |