943 Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set} |
943 Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set} |
944 and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics |
944 and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics |
945 of the specifications (the corresponding $\alpha$-equivalence will differ). We will |
945 of the specifications (the corresponding $\alpha$-equivalence will differ). We will |
946 show this later with an example. |
946 show this later with an example. |
947 |
947 |
948 There are some restrictions we need to impose on binding clasues: the main idea behind |
948 There are some restrictions we need to impose on binding clauses: the main idea behind |
949 these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where |
949 these restrictions is that we obtain a sensible notion of $\alpha$-equivalence where |
950 it is ensured that a bound variable cannot be free at the same time. First, a |
950 it is ensured that a bound variable cannot be free at the same time. First, a |
951 body can only occur in \emph{one} binding clause of a term constructor (this ensures |
951 body can only occur in \emph{one} binding clause of a term constructor (this ensures |
952 that the bound variables of a body cannot be free at the same time by specifying |
952 that the bound variables of a body cannot be free at the same time by specifying |
953 an alternative binder for the body). For |
953 an alternative binder for the body). For |
1913 |
1917 |
1914 |
1918 |
1915 section {* Related Work *} |
1919 section {* Related Work *} |
1916 |
1920 |
1917 text {* |
1921 text {* |
1918 To our knowledge, the earliest usage of general binders in a theorem prover |
1922 To our knowledge the earliest usage of general binders in a theorem prover |
1919 is described in \cite{NaraschewskiNipkow99} about a formalisation of the |
1923 is described in \cite{NaraschewskiNipkow99} about a formalisation of the |
1920 algorithm W. This formalisation implements binding in type schemes using a |
1924 algorithm W. This formalisation implements binding in type schemes using a |
1921 de-Bruijn indices representation. Since type schemes of W contain only a single |
1925 de-Bruijn indices representation. Since type schemes of W contain only a single |
1922 binder, different indices do not refer to different binders (as in the usual |
1926 binder, different indices do not refer to different binders (as in the usual |
1923 de-Bruijn representation), but to different bound variables. A similar idea |
1927 de-Bruijn representation), but to different bound variables. A similar idea |
1924 has been recently explored for general binders in the locally nameless |
1928 has been recently explored for general binders in the locally nameless |
1925 approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist |
1929 approach to binding \cite{chargueraud09}. There, de-Bruijn indices consist |
1926 of two numbers, one referring to the place where a variable is bound and the |
1930 of two numbers, one referring to the place where a variable is bound and the |
1927 other to which variable is bound. The reasoning infrastructure for both |
1931 other to which variable is bound. The reasoning infrastructure for both |
1928 representations of bindings comes for free in theorem provers like Isabelle/HOL or |
1932 representations of bindings comes for free in theorem provers like Isabelle/HOL or |
1929 Coq, as the corresponding term-calculi can be implemented as ``normal'' |
1933 Coq, since the corresponding term-calculi can be implemented as ``normal'' |
1930 datatypes. However, in both approaches it seems difficult to achieve our |
1934 datatypes. However, in both approaches it seems difficult to achieve our |
1931 fine-grained control over the ``semantics'' of bindings (i.e.~whether the |
1935 fine-grained control over the ``semantics'' of bindings (i.e.~whether the |
1932 order of binders should matter, or vacuous binders should be taken into |
1936 order of binders should matter, or vacuous binders should be taken into |
1933 account). To do so, one would require additional predicates that filter out |
1937 account). To do so, one would require additional predicates that filter out |
1934 unwanted terms. Our guess is that such predicates result in rather |
1938 unwanted terms. Our guess is that such predicates result in rather |
1935 intricate formal reasoning. |
1939 intricate formal reasoning. |
1936 |
1940 |
1937 Another representation technique for binding is higher-order abstract syntax |
1941 Another representation technique for binding is higher-order abstract syntax |
1938 (HOAS), which for example is implemented in the Twelf system. This representation |
1942 (HOAS), which for example is implemented in the Twelf system. This representation |
1939 technique supports very elegantly many aspects of \emph{single} binding, and |
1943 technique supports very elegantly many aspects of \emph{single} binding, and |
1940 impressive work is in progress that uses HOAS for mechanising the metatheory |
1944 impressive work has been done that uses HOAS for mechanising the metatheory |
1941 of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple |
1945 of SML~\cite{LeeCraryHarper07}. We are, however, not aware how multiple |
1942 binders of SML are represented in this work. Judging from the submitted |
1946 binders of SML are represented in this work. Judging from the submitted |
1943 Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with |
1947 Twelf-solution for the POPLmark challenge, HOAS cannot easily deal with |
1944 binding constructs where the number of bound variables is not fixed. For |
1948 binding constructs where the number of bound variables is not fixed. For |
1945 example in the second part of this challenge, @{text "Let"}s involve |
1949 example in the second part of this challenge, @{text "Let"}s involve |
1946 patterns that bind multiple variables at once. In such situations, HOAS |
1950 patterns that bind multiple variables at once. In such situations, HOAS |
1947 representations have to resort to the iterated-single-binders-approach with |
1951 representations have to resort to the iterated-single-binders-approach with |
1948 all the unwanted consequences when reasoning about the resulting terms. |
1952 all the unwanted consequences when reasoning about the resulting terms. |
1949 |
1953 |
1950 Two formalisations involving general binders have also been performed in older |
1954 Two formalisations involving general binders have also been performed in older |
1951 versions of Nominal Isabelle (one about Psi-calculi and one about alpgorithm W |
1955 versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W |
1952 \cite{BengtsonParow09, UrbanNipkow09}). Both |
1956 \cite{BengtsonParow09, UrbanNipkow09}). Both |
1953 use the approach based on iterated single binders. Our experience with |
1957 use the approach based on iterated single binders. Our experience with |
1954 the latter formalisation has been disappointing. The major pain arose from |
1958 the latter formalisation has been disappointing. The major pain arose from |
1955 the need to ``unbind'' variables. This can be done in one step with our |
1959 the need to ``unbind'' variables. This can be done in one step with our |
1956 general binders, but needs a cumbersome |
1960 general binders, but needs a cumbersome |
2052 In a slightly different domain (programming with dependent types), the |
2056 In a slightly different domain (programming with dependent types), the |
2053 paper \cite{Altenkirch10} presents a calculus with a notion of |
2057 paper \cite{Altenkirch10} presents a calculus with a notion of |
2054 $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}. |
2058 $\alpha$-equivalence related to our binding mode \isacommand{bind\_res}. |
2055 This definition is similar to the one by Pottier, except that it |
2059 This definition is similar to the one by Pottier, except that it |
2056 has a more operational flavour and calculates a partial (renaming) map. |
2060 has a more operational flavour and calculates a partial (renaming) map. |
2057 In this way they can handle vacous binders. However, their notion of |
2061 In this way they can handle vacuous binders. However, their notion of |
2058 equality between terms also includes rules for $\beta$ and to our |
2062 equality between terms also includes rules for $\beta$ and to our |
2059 knowledge no concrete mathematical result concerning their notion |
2063 knowledge no concrete mathematical result concerning their notion |
2060 of equality has been proved. |
2064 of equality has been proved. |
2061 *} |
2065 *} |
2062 |
2066 |