83 mechanisms for binding single variables have not fared extremely well with the |
83 mechanisms for binding single variables have not fared extremely well with the |
84 more advanced tasks in the POPLmark challenge \cite{challenge05}, because |
84 more advanced tasks in the POPLmark challenge \cite{challenge05}, because |
85 also there one would like to bind multiple variables at once. |
85 also there one would like to bind multiple variables at once. |
86 |
86 |
87 Binding multiple variables has interesting properties that cannot be captured |
87 Binding multiple variables has interesting properties that cannot be captured |
88 easily by iterating single binders. For example in case of type-schemes we do not |
88 easily by iterating single binders. For example in the case of type-schemes we do not |
89 want to make a distinction about the order of the bound variables. Therefore |
89 want to make a distinction about the order of the bound variables. Therefore |
90 we would like to regard the following two type-schemes as alpha-equivalent |
90 we would like to regard the following two type-schemes as alpha-equivalent |
91 % |
91 % |
92 \begin{equation}\label{ex1} |
92 \begin{equation}\label{ex1} |
93 @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"} |
93 @{text "\<forall>{x, y}. x \<rightarrow> y \<approx>\<^isub>\<alpha> \<forall>{y, x}. y \<rightarrow> x"} |
181 |
181 |
182 \noindent |
182 \noindent |
183 where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"} |
183 where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"} |
184 becomes bound in @{text s}. In this representation the term |
184 becomes bound in @{text s}. In this representation the term |
185 \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal |
185 \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal |
186 instance, but the lengths of two lists do not agree. To exclude such terms, |
186 instance, but the lengths of the two lists do not agree. To exclude such terms, |
187 additional predicates about well-formed |
187 additional predicates about well-formed |
188 terms are needed in order to ensure that the two lists are of equal |
188 terms are needed in order to ensure that the two lists are of equal |
189 length. This can result into very messy reasoning (see for |
189 length. This can result in very messy reasoning (see for |
190 example~\cite{BengtsonParow09}). To avoid this, we will allow type |
190 example~\cite{BengtsonParow09}). To avoid this, we will allow type |
191 specifications for $\mathtt{let}$s as follows |
191 specifications for $\mathtt{let}$s as follows |
192 % |
192 % |
193 \begin{center} |
193 \begin{center} |
194 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
194 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
218 clause states to bind in @{text s} all the names the function @{text |
218 clause states to bind in @{text s} all the names the function @{text |
219 "bn(as)"} returns. This style of specifying terms and bindings is heavily |
219 "bn(as)"} returns. This style of specifying terms and bindings is heavily |
220 inspired by the syntax of the Ott-tool \cite{ott-jfp}. |
220 inspired by the syntax of the Ott-tool \cite{ott-jfp}. |
221 |
221 |
222 However, we will not be able to cope with all specifications that are |
222 However, we will not be able to cope with all specifications that are |
223 allowed by Ott. One reason is that Ott lets the user to specify ``empty'' |
223 allowed by Ott. One reason is that Ott lets the user specify ``empty'' |
224 types like |
224 types like |
225 |
225 |
226 \begin{center} |
226 \begin{center} |
227 @{text "t ::= t t | \<lambda>x. t"} |
227 @{text "t ::= t t | \<lambda>x. t"} |
228 \end{center} |
228 \end{center} |
702 @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity |
702 @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity |
703 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
703 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
704 $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no |
704 $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no |
705 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
705 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
706 (similarly for $\approx_{\textit{list}}$). It can also relatively easily be |
706 (similarly for $\approx_{\textit{list}}$). It can also relatively easily be |
707 shown that all tree notions of alpha-equivalence coincide, if we only |
707 shown that all three notions of alpha-equivalence coincide, if we only |
708 abstract a single atom. |
708 abstract a single atom. |
709 |
709 |
710 In the rest of this section we are going to introduce three abstraction |
710 In the rest of this section we are going to introduce three abstraction |
711 types. For this we define |
711 types. For this we define |
712 % |
712 % |
1117 Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just |
1117 Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, just |
1118 re-arranging the arguments of |
1118 re-arranging the arguments of |
1119 term-constructors so that binders and their bodies are next to each other will |
1119 term-constructors so that binders and their bodies are next to each other will |
1120 result in inadequate representations. Therefore we will first |
1120 result in inadequate representations. Therefore we will first |
1121 extract datatype definitions from the specification and then define |
1121 extract datatype definitions from the specification and then define |
1122 expicitly an alpha-equivalence relation over them. |
1122 explicitly an alpha-equivalence relation over them. |
1123 |
1123 |
1124 |
1124 |
1125 The datatype definition can be obtained by stripping off the |
1125 The datatype definition can be obtained by stripping off the |
1126 binding clauses and the labels from the types. We also have to invent |
1126 binding clauses and the labels from the types. We also have to invent |
1127 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1127 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1150 % |
1150 % |
1151 \begin{equation}\label{ceqvt} |
1151 \begin{equation}\label{ceqvt} |
1152 @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"} |
1152 @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"} |
1153 \end{equation} |
1153 \end{equation} |
1154 |
1154 |
1155 The first non-trivial step we have to perform is the generation free-variable |
1155 The first non-trivial step we have to perform is the generation of free-variable |
1156 functions from the specifications. For atomic types we define the auxilary |
1156 functions from the specifications. For atomic types we define the auxilary |
1157 free variable functions: |
1157 free variable functions: |
1158 |
1158 |
1159 \begin{center} |
1159 \begin{center} |
1160 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
1160 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
1453 @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant. |
1453 @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant. |
1454 \end{lemma} |
1454 \end{lemma} |
1455 |
1455 |
1456 \begin{proof} |
1456 \begin{proof} |
1457 The proof is by mutual induction over the definitions. The non-trivial |
1457 The proof is by mutual induction over the definitions. The non-trivial |
1458 cases involve premises build up by $\approx_{\textit{set}}$, |
1458 cases involve premises built up by $\approx_{\textit{set}}$, |
1459 $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They |
1459 $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They |
1460 can be dealt with as in Lemma~\ref{alphaeq}. |
1460 can be dealt with as in Lemma~\ref{alphaeq}. |
1461 \end{proof} |
1461 \end{proof} |
1462 |
1462 |
1463 \noindent |
1463 \noindent |
1524 \begin{center} |
1524 \begin{center} |
1525 @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "} |
1525 @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>1 y\<^isub>1 \<dots> P\<^bsub>ty\<AL>\<^esub>\<^isub>n y\<^isub>n "} |
1526 \end{center} |
1526 \end{center} |
1527 |
1527 |
1528 \noindent |
1528 \noindent |
1529 for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties |
1529 for all @{text "y\<^isub>i"} whereby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties |
1530 defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of |
1530 defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of |
1531 these induction principles look |
1531 these induction principles look |
1532 as follows |
1532 as follows |
1533 |
1533 |
1534 \begin{center} |
1534 \begin{center} |
1538 \noindent |
1538 \noindent |
1539 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. |
1539 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}. |
1540 Next we lift the permutation operations defined in \eqref{ceqvt} for |
1540 Next we lift the permutation operations defined in \eqref{ceqvt} for |
1541 the raw term-constructors @{text "C"}. These facts contain, in addition |
1541 the raw term-constructors @{text "C"}. These facts contain, in addition |
1542 to the term-constructors, also permutation operations. In order to make the |
1542 to the term-constructors, also permutation operations. In order to make the |
1543 lifting to go through, |
1543 lifting go through, |
1544 we have to know that the permutation operations are respectful |
1544 we have to know that the permutation operations are respectful |
1545 w.r.t.~alpha-equivalence. This amounts to showing that the |
1545 w.r.t.~alpha-equivalence. This amounts to showing that the |
1546 alpha-equivalence relations are equivariant, which we already established |
1546 alpha-equivalence relations are equivariant, which we already established |
1547 in Lemma~\ref{equiv}. As a result we can establish the equations |
1547 in Lemma~\ref{equiv}. As a result we can establish the equations |
1548 |
1548 |
1565 \end{tabular}} |
1565 \end{tabular}} |
1566 \end{equation} |
1566 \end{equation} |
1567 |
1567 |
1568 \noindent |
1568 \noindent |
1569 which can be established by induction on @{text "\<approx>ty"}. Whereas the first |
1569 which can be established by induction on @{text "\<approx>ty"}. Whereas the first |
1570 property is always true by the way how we defined the free-variable |
1570 property is always true by the way we defined the free-variable |
1571 functions for types, the second and third do \emph{not} hold in general. There is, in principle, |
1571 functions for types, the second and third do \emph{not} hold in general. There is, in principle, |
1572 the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound |
1572 the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound |
1573 variable. Then the third property is just not true. However, our |
1573 variable. Then the third property is just not true. However, our |
1574 restrictions imposed on the binding functions |
1574 restrictions imposed on the binding functions |
1575 exclude this possibility. |
1575 exclude this possibility. |
1862 \hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"} |
1862 \hspace{15mm}@{text "Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"} |
1863 \end{tabular} |
1863 \end{tabular} |
1864 \end{center} |
1864 \end{center} |
1865 |
1865 |
1866 \noindent |
1866 \noindent |
1867 So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally |
1867 So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally |
1868 establish |
1868 establish |
1869 |
1869 |
1870 \begin{center} |
1870 \begin{center} |
1871 @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"} |
1871 @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"} |
1872 \end{center} |
1872 \end{center} |
1892 |
1892 |
1893 Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, |
1893 Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, |
1894 we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. |
1894 we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. |
1895 This completes the proof showing that the strong induction principle derives from |
1895 This completes the proof showing that the strong induction principle derives from |
1896 the weak induction principle. For the moment we can derive the difficult cases of |
1896 the weak induction principle. For the moment we can derive the difficult cases of |
1897 the strong induction principles only by hand, but they are very schematically |
1897 the strong induction principles only by hand, but they are very schematic |
1898 so that with little effort we can even derive them for |
1898 so that with little effort we can even derive them for |
1899 Core-Haskell given in Figure~\ref{nominalcorehas}. |
1899 Core-Haskell given in Figure~\ref{nominalcorehas}. |
1900 *} |
1900 *} |
1901 |
1901 |
1902 |
1902 |