13 (*>*) |
13 (*>*) |
14 |
14 |
15 section {* Introduction *} |
15 section {* Introduction *} |
16 |
16 |
17 text {* |
17 text {* |
18 So far, Nominal Isabelle provided a mechanism to construct |
18 So far, Nominal Isabelle provides a mechanism for constructing |
19 automatically alpha-equated lambda terms sich as |
19 automatically alpha-equated terms such as |
20 |
20 |
21 \begin{center} |
21 \begin{center} |
22 $t ::= x \mid t\;t \mid \lambda x. t$ |
22 $t ::= x \mid t\;t \mid \lambda x. t$ |
23 \end{center} |
23 \end{center} |
24 |
24 |
25 \noindent |
25 \noindent |
26 For such calculi, it derived automatically a convenient reasoning |
26 For such terms it derives automatically a reasoning |
27 infrastructure. With this it has been used to formalise an equivalence |
27 infrastructure, which has been used in formalisations of an equivalence |
28 checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
28 checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
29 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
29 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
30 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result |
30 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result |
31 for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been |
31 for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been |
32 used by Pollack for formalisations in the locally-nameless approach to |
32 used by Pollack for formalisations in the locally-nameless approach to |
33 binding \cite{SatoPollack10}. |
33 binding \cite{SatoPollack10}. |
34 |
34 |
35 However, Nominal Isabelle has fared less well in a formalisation of |
35 However, Nominal Isabelle fared less well in a formalisation of |
36 the algorithm W \cite{UrbanNipkow09} where types and type-schemes |
36 the algorithm W \cite{UrbanNipkow09}, where types and type-schemes |
37 are represented by |
37 are of the form |
38 |
38 |
39 \begin{center} |
39 \begin{center} |
40 \begin{tabular}{l} |
40 \begin{tabular}{l} |
41 $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ |
41 $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ |
42 \end{tabular} |
42 \end{tabular} |
43 \end{center} |
43 \end{center} |
44 |
44 |
45 \noindent |
45 \noindent |
46 While it is possible to formalise the finite set of variables that are |
46 and the quantification abstracts over a finite (possibly empty) set of type variables. |
47 abstracted in a type-scheme by iterating single abstractions, it leads to a very |
47 While it is possible to formalise such abstractions by iterating single bindings, |
48 clumsy formalisation. This need of iterating single binders for representing |
48 it leads to a very clumsy formalisation of W. This need of iterating single binders |
49 multiple binders is also the reason why Nominal Isabelle and other theorem |
49 for representing multiple binders is also the reason why Nominal Isabelle and other |
50 provers have so far not fared very well with the more advanced tasks in the POPLmark |
50 theorem provers have not fared extremely well with the more advanced tasks |
51 challenge, because also there one would like to abstract several variables |
51 in the POPLmark challenge \cite{challenge05}, because also there one would be able |
|
52 to aviod clumsy reasoning if there were a mechanisms for abstracting several variables |
52 at once. |
53 at once. |
53 |
54 |
54 There are interesting points to note with binders that abstract multiple |
55 To see this, let us point out some interesting properties of binders abstracting multiple |
55 variables. First in the case of type-schemes we do not like to make a distinction |
56 variables. First, in the case of type-schemes, we do not like to make a distinction |
56 about the order of the binders. So we would like to regard the following two |
57 about the order of the bound variables. Therefore we would like to regard the following two |
57 type-schemes as alpha-equivalent: |
58 type-schemes as alpha-equivalent |
58 |
59 |
59 \begin{center} |
60 \begin{center} |
60 $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ |
61 $\forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x$ |
61 \end{center} |
62 \end{center} |
62 |
63 |
63 \noindent |
64 \noindent |
64 but assuming $x$, $y$ and $z$ are distinct, the following two should be \emph{not} |
65 but the following two should \emph{not} be alpha-equivalent |
65 alpha-equivalent: |
|
66 |
66 |
67 \begin{center} |
67 \begin{center} |
68 $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ |
68 $\forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z$ |
69 \end{center} |
69 \end{center} |
70 |
70 |
71 \noindent |
71 \noindent |
72 However we do like to regard type-schemes as alpha-equivalent, if they |
72 assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as |
73 differ only on \emph{vacuous} binders, such as |
73 alpha-equivalent, if they differ only on \emph{vacuous} binders, such as |
74 |
74 |
75 \begin{center} |
75 \begin{center} |
76 $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ |
76 $\forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y$ |
77 \end{center} |
77 \end{center} |
78 |
78 |
79 \noindent |
79 \noindent |
80 In this paper we will give a general abstraction mechanism and assciated notion of alpha-equivalence |
80 In this paper we will give a general abstraction mechanism and associated |
81 which can be used to represent type-schemes. The difficulty in finding the notion of alpha-equivalence |
81 notion of alpha-equivalence that can be used to faithfully represent |
82 can be appreciated by considering that the definition given by Leroy in \cite{Leroy92} is incorrect |
82 type-schemes in Nominal Isabelle. The difficulty of finding the right notion |
83 (it omits a side-condition). |
83 for alpha-equivalence in this case can be appreciated by considering that the |
|
84 definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
|
85 |
|
86 |
84 |
87 |
85 However, the notion of alpha-equivalence that is preserved by vacuous binders is not |
88 However, the notion of alpha-equivalence that is preserved by vacuous binders is not |
86 alway wanted. For example in constructs like |
89 alway wanted. For example in terms like |
87 |
90 |
88 \begin{center} |
91 \begin{center} |
89 $\LET x = 3 \AND y = 2 \IN x \backslash y \END$ |
92 $\LET x = 3 \AND y = 2 \IN x\,\backslash\,y \END$ |
90 \end{center} |
93 \end{center} |
91 |
94 |
92 \noindent |
95 \noindent |
93 we might not care in which order the associations $x = 3$ and $y = 2$ are |
96 we might not care in which order the assignments $x = 3$ and $y = 2$ are |
94 given, but it would be unusual to regard this term as alpha-equivalent with |
97 given, but it would be unusual to regard the above term as alpha-equivalent |
95 |
98 with |
96 \begin{center} |
99 |
97 $\LET x = 3 \AND y = 2 \AND z = loop \IN x \backslash y \END$ |
100 \begin{center} |
98 \end{center} |
101 $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$ |
99 |
102 \end{center} |
100 \noindent |
103 |
101 We will provide a separate abstraction mechanism for this case where the |
104 \noindent |
102 order of binders does not matter, but the ``cardinality'' of the binders |
105 Therefore we will also provide a separate abstraction mechanism for cases |
103 has to be the same. |
106 in which the order of binders does not matter, but the ``cardinality'' of the |
104 |
107 binders has to be the same. |
105 However, this is still not sufficient for covering language constructs frequently |
108 |
106 occuring in programming language research. For example in patters like |
109 However, we found that this is still not sufficient for covering language |
107 |
110 constructs frequently occuring in programming language research. For example |
108 \begin{center} |
111 in $\mathtt{let}$s involving patterns |
109 $\LET (x, y) = (3, 2) \IN x \backslash y \END$ |
112 |
|
113 \begin{center} |
|
114 $\LET (x, y) = (3, 2) \IN x\,\backslash\,y \END$ |
110 \end{center} |
115 \end{center} |
111 |
116 |
112 \noindent |
117 \noindent |
113 we want to bind all variables from the pattern (there might be an arbitrary |
118 we want to bind all variables from the pattern (there might be an arbitrary |
114 number of them) inside the body of the let, but we also care about the order |
119 number of them) inside the body of the $\mathtt{let}$, but we also care about |
115 of these variables, since we do not want to identify this term with |
120 the order of these variables, since we do not want to identify the above term |
116 |
121 with |
117 \begin{center} |
122 |
118 $\LET (y, x) = (3, 2) \IN x \backslash y \END$ |
123 \begin{center} |
119 \end{center} |
124 $\LET (y, x) = (3, 2) \IN x\,\backslash y\,\END$ |
120 |
125 \end{center} |
121 \noindent |
126 |
122 Therefore we have identified three abstraction mechanisms for multiple binders |
127 \noindent |
123 and allow the user to chose which one is intended. |
128 As a result, we provide three general abstraction mechanisms for multiple binders |
124 |
129 and allow the user to chose which one is intended when formalising a |
125 By providing general abstraction mechanisms that allow the binding of multiple |
130 programming language calculus. |
126 variables, we have to work around aproblem that has been first pointed out |
131 |
127 by Pottier in \cite{Pottier}: in let-constructs such as |
132 By providing these general abstraction mechanisms, however, we have to work around |
|
133 a problem that has been pointed out by Pottier in \cite{Pottier06}: in |
|
134 $\mathtt{let}$-constructs of the form |
128 |
135 |
129 \begin{center} |
136 \begin{center} |
130 $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ |
137 $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ |
131 \end{center} |
138 \end{center} |
132 |
139 |
133 \noindent |
140 \noindent |
134 where the $x_i$ are bound in $s$. In this term we might not care about the order in |
141 which bind all the $x_i$ in $s$, we might not care about the order in |
135 which the $x_i = t_i$ are given, but we do care about the information that there are |
142 which the $x_i = t_i$ are given, but we do care about the information that there are |
136 as many $x_i$ as there are $t_i$. We lose this information if we specify the |
143 as many $x_i$ as there are $t_i$. We lose this information if we represent the |
137 $\mathtt{let}$-constructor as something like |
144 $\mathtt{let}$-constructor as something like |
138 |
145 |
139 \begin{center} |
146 \begin{center} |
140 $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$ |
147 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ |
141 \end{center} |
148 \end{center} |
142 |
149 |
143 \noindent |
150 \noindent |
144 where the $[\_].\_$ indicates that a list of variables become bound |
151 where the $[\_\!\_].\_\!\_$ indicates that a list of variables becomes bound |
145 in $s$. In this representation we need additional predicates to ensure |
152 in $s$. In this representation we need additional predicates to ensure |
146 that the two lists are of equal length. This can result into very |
153 that the two lists are of equal length. This can result into very |
147 elaborate reasoning (see \cite{BengtsonParow09}). |
154 unintelligible reasoning (see for example~\cite{BengtsonParow09}). |
148 |
155 |
149 |
156 |
150 |
157 |
151 |
158 |
152 |
159 |