113 where @{text z} does not occur freely in the type. In this paper we will |
113 where @{text z} does not occur freely in the type. In this paper we will |
114 give a general binding mechanism and associated notion of alpha-equivalence |
114 give a general binding mechanism and associated notion of alpha-equivalence |
115 that can be used to faithfully represent this kind of binding in Nominal |
115 that can be used to faithfully represent this kind of binding in Nominal |
116 Isabelle. The difficulty of finding the right notion for alpha-equivalence |
116 Isabelle. The difficulty of finding the right notion for alpha-equivalence |
117 can be appreciated in this case by considering that the definition given by |
117 can be appreciated in this case by considering that the definition given by |
118 Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
118 Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). A related |
|
119 notion of alpha-equivalence that allows vacuous binders, there called weakening |
|
120 of contexts, is defined in for the $\Pi\Sigma$-calculus \cite{Altenkirch10}. |
119 |
121 |
120 However, the notion of alpha-equivalence that is preserved by vacuous |
122 However, the notion of alpha-equivalence that is preserved by vacuous |
121 binders is not always wanted. For example in terms like |
123 binders is not always wanted. For example in terms like |
122 % |
124 % |
123 \begin{equation}\label{one} |
125 \begin{equation}\label{one} |
152 we do not want to regard \eqref{two} as alpha-equivalent with |
154 we do not want to regard \eqref{two} as alpha-equivalent with |
153 % |
155 % |
154 \begin{center} |
156 \begin{center} |
155 @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"} |
157 @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"} |
156 \end{center} |
158 \end{center} |
157 |
159 % |
158 \noindent |
160 \noindent |
159 As a result, we provide three general binding mechanisms each of which binds |
161 As a result, we provide three general binding mechanisms each of which binds |
160 multiple variables at once, and let the user chose which one is intended |
162 multiple variables at once, and let the user chose which one is intended |
161 when formalising a term-calculus. |
163 when formalising a term-calculus. |
162 |
164 |
362 {\bf Contributions:} We provide new definitions for when terms |
364 {\bf Contributions:} We provide new definitions for when terms |
363 involving multiple binders are alpha-equivalent. These definitions are |
365 involving multiple binders are alpha-equivalent. These definitions are |
364 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic |
366 inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic |
365 proofs, we establish a reasoning infrastructure for alpha-equated |
367 proofs, we establish a reasoning infrastructure for alpha-equated |
366 terms, including properties about support, freshness and equality |
368 terms, including properties about support, freshness and equality |
367 conditions for alpha-equated terms. We are also able to derive, for the moment |
369 conditions for alpha-equated terms. We are also able to derive strong |
368 only manually, strong induction principles that |
370 induction principles that have the variable convention already built in. |
369 have the variable convention already built in. |
|
370 |
371 |
371 \begin{figure} |
372 \begin{figure} |
372 \begin{boxedminipage}{\linewidth} |
373 \begin{boxedminipage}{\linewidth} |
373 \begin{center} |
374 \begin{center} |
374 \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l} |
375 \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l} |
2015 can be indicated with some special constructs, written @{text "inner"} and |
2016 can be indicated with some special constructs, written @{text "inner"} and |
2016 @{text "outer"}. With this, it seems, our and his specifications can be |
2017 @{text "outer"}. With this, it seems, our and his specifications can be |
2017 inter-translated, but we have not proved this. However, we believe the |
2018 inter-translated, but we have not proved this. However, we believe the |
2018 binding specifications in the style of Ott are a more natural way for |
2019 binding specifications in the style of Ott are a more natural way for |
2019 representing terms involving bindings. Pottier gives a definition for |
2020 representing terms involving bindings. Pottier gives a definition for |
2020 alpha-equivalence, which is similar to our binding mod \isacommand{bind}. |
2021 alpha-equivalence, which is similar to our binding mode \isacommand{bind}. |
2021 Although he uses also a permutation in case of abstractions, his |
2022 Although he uses also a permutation in case of abstractions, his |
2022 definition is rather different from ours. He proves that his notion |
2023 definition is rather different from ours. He proves that his notion |
2023 of alpha-equivalence is indeed a equivalence relation, but a complete |
2024 of alpha-equivalence is indeed a equivalence relation, but a complete |
2024 reasoning infrastructure is well beyond the purposes of his language. |
2025 reasoning infrastructure is well beyond the purposes of his language. |
|
2026 In a slightly different domain (programming with dependent types), the |
|
2027 paper \cite{Altenkirch10} presents a calculus with a notion of |
|
2028 alpha-equivalence related to our binding mode \isacommand{bind\_res}. |
|
2029 This definition is similar to the one by Pottier, except that it |
|
2030 has a more operational flavour and calculates a partial (renaming) map. |
|
2031 In this way they can handle vacous binders. However, their notion of |
|
2032 equality between terms also includes rules for $\beta$ and to our |
|
2033 knowledge no concrete mathematical result concerning their notion |
|
2034 of equality has been proved. |
2025 *} |
2035 *} |
2026 |
2036 |
2027 section {* Conclusion *} |
2037 section {* Conclusion *} |
2028 |
2038 |
2029 text {* |
2039 text {* |