Paper/Paper.thy
changeset 2342 f296ef291ca9
parent 2341 f659ce282610
child 2343 36aeb97fabb0
equal deleted inserted replaced
2341:f659ce282610 2342:f296ef291ca9
   851   laborious to write custom ML-code that derives automatically such properties 
   851   laborious to write custom ML-code that derives automatically such properties 
   852   for every term-constructor that binds some atoms. Also the generality of
   852   for every term-constructor that binds some atoms. Also the generality of
   853   the definitions for $\alpha$-equivalence will help us in the next section.
   853   the definitions for $\alpha$-equivalence will help us in the next section.
   854 *}
   854 *}
   855 
   855 
   856 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
   856 section {* Specifying General Binders\label{sec:spec} *}
   857 
   857 
   858 text {*
   858 text {*
   859   Our choice of syntax for specifications is influenced by the existing
   859   Our choice of syntax for specifications is influenced by the existing
   860   datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
   860   datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
   861   Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
   861   Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
   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
  1119   \end{center}
  1119   \end{center}
  1120 
  1120 
  1121   \noindent 
  1121   \noindent 
  1122   The point of completion is that we can make definitions over the binding
  1122   The point of completion is that we can make definitions over the binding
  1123   clauses and be sure to have captured all arguments of a term constructor. 
  1123   clauses and be sure to have captured all arguments of a term constructor. 
  1124 
  1124 *}
       
  1125 
       
  1126 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
       
  1127 
       
  1128 text {*
  1125   Having dealt with all syntax matters, the problem now is how we can turn
  1129   Having dealt with all syntax matters, the problem now is how we can turn
  1126   specifications into actual type definitions in Isabelle/HOL and then
  1130   specifications into actual type definitions in Isabelle/HOL and then
  1127   establish a reasoning infrastructure for them. As
  1131   establish a reasoning infrastructure for them. As
  1128   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 
  1132   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just 
  1129   re-arranging the arguments of
  1133   re-arranging the arguments of
  1183   \noindent
  1187   \noindent
  1184   The reason for this setup is that in a deep binder not all atoms have to be
  1188   The reason for this setup is that in a deep binder not all atoms have to be
  1185   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
  1189   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
  1186   that calculates those unbound atoms. 
  1190   that calculates those unbound atoms. 
  1187 
  1191 
  1188   For atomic types we define the auxilary
  1192   For atomic types we define the auxiliary
  1189   free variable functions:
  1193   free variable functions:
  1190 
  1194 
  1191   \begin{center}
  1195   \begin{center}
  1192   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  1196   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  1193   @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\
  1197   @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\
  1283   \end{center}
  1287   \end{center}
  1284 
  1288 
  1285   \noindent
  1289   \noindent
  1286   Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
  1290   Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}
  1287   and @{text "ACons"}, the corresponding free-variable function @{text
  1291   and @{text "ACons"}, the corresponding free-variable function @{text
  1288   "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
  1292   "fv\<^bsub>assn\<^esub>"} returns all atoms occurring in an assignment. The
  1289   binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
  1293   binding only takes place in @{text Let} and @{text "Let_rec"}. In the @{text
  1290   "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
  1294   "Let"}-clause we want to bind all atoms given by @{text "set (bn as)"} in
  1291   @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
  1295   @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
  1292   "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
  1296   "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
  1293   free in @{text "as"}. This is what the purpose of the function @{text
  1297   free in @{text "as"}. This is what the purpose of the function @{text
  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 
  2113   can be easily extended to accommodate them.
  2117   can be easily extended to accommodate them.
  2114 
  2118 
  2115   \medskip
  2119   \medskip
  2116   \noindent
  2120   \noindent
  2117   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
  2121   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
  2118   many discussions about Nominal Isabelle. We thank Peter Sewell for 
  2122   many discussions about Nominal Isabelle. We also thank Peter Sewell for 
  2119   making the informal notes \cite{SewellBestiary} available to us and 
  2123   making the informal notes \cite{SewellBestiary} available to us and 
  2120   also for patiently explaining some of the finer points of the work on the Ott-tool. We
  2124   also for patiently explaining some of the finer points of the work on the Ott-tool.
  2121   also thank Stephanie Weirich for suggesting to separate the subgrammars
  2125   Stephanie Weirich suggested to separate the subgrammars
  2122   of kinds and types in our Core-Haskell example.  
  2126   of kinds and types in our Core-Haskell example.  
  2123 
  2127 
  2124 
       
  2125   * Conference of Altenkirch *
       
  2126 *}
  2128 *}
  2127 
  2129 
  2128 (*<*)
  2130 (*<*)
  2129 end
  2131 end
  2130 (*>*)
  2132 (*>*)