equal
deleted
inserted
replaced
1352 |
1352 |
1353 \noindent |
1353 \noindent |
1354 Recall that @{text ANil} and @{text "ACons"} have no |
1354 Recall that @{text ANil} and @{text "ACons"} have no |
1355 binding clause in the specification. The corresponding free-atom |
1355 binding clause in the specification. The corresponding free-atom |
1356 function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms |
1356 function @{text "fa\<^bsub>assn\<^esub>"} therefore returns all free atoms |
1357 occurring in an assignment (in case of @{text "ACons"}, they are given by |
1357 occurring in an assignment (in case of @{text "ACons"}, they are given in |
1358 calls to @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). |
1358 terms of @{text supp}, @{text "fa\<^bsub>trm\<^esub>"} and @{text "fa\<^bsub>assn\<^esub>"}). |
1359 The binding only takes place in @{text Let} and |
1359 The binding only takes place in @{text Let} and |
1360 @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies |
1360 @{text "Let_rec"}. In case of @{text "Let"}, the binding clause specifies |
1361 that all atoms given by @{text "set (bn as)"} have to be bound in @{text |
1361 that all atoms given by @{text "set (bn as)"} have to be bound in @{text |
1362 t}. Therefore we have to subtract @{text "set (bn as)"} from @{text |
1362 t}. Therefore we have to subtract @{text "set (bn as)"} from @{text |
1363 "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are |
1363 "fa\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are |
1590 $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of |
1590 $\approx_{\textit{bn}}$: the latter only ``tracks'' $\alpha$-equivalence of |
1591 the components in an assignment that are \emph{not} bound. This is needed in the |
1591 the components in an assignment that are \emph{not} bound. This is needed in the |
1592 in the clause for @{text "Let"} (which is has |
1592 in the clause for @{text "Let"} (which is has |
1593 a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant |
1593 a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant |
1594 to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, |
1594 to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, |
1595 because there everything from the assignment is under the binder. |
1595 because there all components of an assignment are ``under'' the binder. |
1596 *} |
1596 *} |
1597 |
1597 |
1598 section {* Establishing the Reasoning Infrastructure *} |
1598 section {* Establishing the Reasoning Infrastructure *} |
1599 |
1599 |
1600 text {* |
1600 text {* |
2062 |
2062 |
2063 text {* |
2063 text {* |
2064 To our knowledge the earliest usage of general binders in a theorem prover |
2064 To our knowledge the earliest usage of general binders in a theorem prover |
2065 is described in \cite{NaraschewskiNipkow99} about a formalisation of the |
2065 is described in \cite{NaraschewskiNipkow99} about a formalisation of the |
2066 algorithm W. This formalisation implements binding in type schemes using a |
2066 algorithm W. This formalisation implements binding in type schemes using a |
2067 de-Bruijn indices representation. Since type schemes of W contain only a single |
2067 de-Bruijn indices representation. Since type schemes in W contain only a single |
2068 binder, different indices do not refer to different binders (as in the usual |
2068 place where variables are bound, different indices do not refer to different binders (as in the usual |
2069 de-Bruijn representation), but to different bound variables. A similar idea |
2069 de-Bruijn representation), but to different bound variables. A similar idea |
2070 has been recently explored for general binders in the locally nameless |
2070 has been recently explored for general binders in the locally nameless |
2071 approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist |
2071 approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist |
2072 of two numbers, one referring to the place where a variable is bound and the |
2072 of two numbers, one referring to the place where a variable is bound and the |
2073 other to which variable is bound. The reasoning infrastructure for both |
2073 other to which variable is bound. The reasoning infrastructure for both |
2091 example in the second part of this challenge, @{text "Let"}s involve |
2091 example in the second part of this challenge, @{text "Let"}s involve |
2092 patterns that bind multiple variables at once. In such situations, HOAS |
2092 patterns that bind multiple variables at once. In such situations, HOAS |
2093 representations have to resort to the iterated-single-binders-approach with |
2093 representations have to resort to the iterated-single-binders-approach with |
2094 all the unwanted consequences when reasoning about the resulting terms. |
2094 all the unwanted consequences when reasoning about the resulting terms. |
2095 |
2095 |
2096 Two formalisations involving general binders have also been performed in older |
2096 In a similar fashion, two formalisations involving general binders have been |
|
2097 performed in older |
2097 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W |
2098 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W |
2098 \cite{BengtsonParow09, UrbanNipkow09}). Both |
2099 \cite{BengtsonParow09, UrbanNipkow09}). Both |
2099 use the approach based on iterated single binders. Our experience with |
2100 use the approach based on iterated single binders. Our experience with |
2100 the latter formalisation has been disappointing. The major pain arose from |
2101 the latter formalisation has been disappointing. The major pain arose from |
2101 the need to ``unbind'' variables. This can be done in one step with our |
2102 the need to ``unbind'' variables. This can be done in one step with our |