42 $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ |
42 $T ::= x \mid T \rightarrow T$ \hspace{5mm} $S ::= \forall \{x_1,\ldots, x_n\}. T$ |
43 \end{tabular} |
43 \end{tabular} |
44 \end{center} |
44 \end{center} |
45 |
45 |
46 \noindent |
46 \noindent |
47 and the quantification binds at once a finite (possibly empty) set of |
47 and the quantification $\forall$ binds a finite (possibly empty) set of |
48 type-variables. While it is possible to implement this kind of more general |
48 type-variables. While it is possible to implement this kind of more general |
49 binders by iterating single binders, this leads to a rather clumsy |
49 binders by iterating single binders, this leads to a rather clumsy |
50 formalisation of W. The need of iterating single binders is also one reason |
50 formalisation of W. The need of iterating single binders is also one reason |
51 why Nominal Isabelle and similar theorem provers that only provide |
51 why Nominal Isabelle and similar theorem provers that only provide |
52 mechanisms for binding single variables have not fared extremely well with the |
52 mechanisms for binding single variables have not fared extremely well with the |
84 this kind of binding in Nominal Isabelle. The difficulty of finding the right notion |
84 this kind of binding in Nominal Isabelle. The difficulty of finding the right notion |
85 for alpha-equivalence in this case can be appreciated by considering that the |
85 for alpha-equivalence in this case can be appreciated by considering that the |
86 definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
86 definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
87 |
87 |
88 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 |
89 alway wanted. For example in terms like |
89 always wanted. For example in terms like |
90 |
90 |
91 \begin{equation}\label{one} |
91 \begin{equation}\label{one} |
92 \LET x = 3 \AND y = 2 \IN x\,-\,y \END |
92 \LET x = 3 \AND y = 2 \IN x\,-\,y \END |
93 \end{equation} |
93 \end{equation} |
94 |
94 |
115 \end{equation} |
115 \end{equation} |
116 |
116 |
117 \noindent |
117 \noindent |
118 we want to bind all variables from the pattern inside the body of the |
118 we want to bind all variables from the pattern inside the body of the |
119 $\mathtt{let}$, but we also care about the order of these variables, since |
119 $\mathtt{let}$, but we also care about the order of these variables, since |
120 we do not want to identify \eqref{two} with |
120 we do not want to regard \eqref{two} as alpha-equivalent with |
121 |
121 |
122 \begin{center} |
122 \begin{center} |
123 $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ |
123 $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ |
124 \end{center} |
124 \end{center} |
125 |
125 |
126 \noindent |
126 \noindent |
127 As a result, we provide three general binding mechanisms each of which binds multiple |
127 As a result, we provide three general binding mechanisms each of which binds multiple |
128 variables at once, and we let the user chose which one is intended when formalising a |
128 variables at once, and let the user chose which one is intended when formalising a |
129 programming language calculus. |
129 programming language calculus. |
130 |
130 |
131 By providing these general binding mechanisms, however, we have to work around |
131 By providing these general binding mechanisms, however, we have to work around |
132 a problem that has been pointed out by Pottier in \cite{Pottier06}: in |
132 a problem that has been pointed out by Pottier in \cite{Pottier06}: in |
133 $\mathtt{let}$-constructs of the form |
133 $\mathtt{let}$-constructs of the form |
145 \begin{center} |
145 \begin{center} |
146 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ |
146 $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ |
147 \end{center} |
147 \end{center} |
148 |
148 |
149 \noindent |
149 \noindent |
150 where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become |
150 where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound |
151 bound in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$} |
151 in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$} |
152 would be perfectly legal instance, and so one needs additional predicates about terms |
152 would be a perfectly legal instance. To exclude such terms an additional |
153 to ensure that the two lists are of equal length. This can result into very |
153 predicate about well-formed terms is needed in order to ensure that the two |
154 messy reasoning (see for example~\cite{BengtsonParow09}). |
154 lists are of equal length. This can result into very messy reasoning (see |
155 To avoid this, we will allowto specify for example $\mathtt{let}$s |
155 for example~\cite{BengtsonParow09}). To avoid this, we will allow specifications |
156 as follows |
156 for $\mathtt{let}$s as follows |
157 |
157 |
158 \begin{center} |
158 \begin{center} |
159 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
159 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
160 $trm$ & $=$ & \ldots\\ |
160 $trm$ & $=$ & \ldots\\ |
161 & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] |
161 & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] |
165 \end{center} |
165 \end{center} |
166 |
166 |
167 \noindent |
167 \noindent |
168 where $assn$ is an auxiliary type representing a list of assignments |
168 where $assn$ is an auxiliary type representing a list of assignments |
169 and $bn$ an auxiliary function identifying the variables to be bound by |
169 and $bn$ an auxiliary function identifying the variables to be bound by |
170 the $\mathtt{let}$. This function can be defined by recursion over $assn$ as |
170 the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows |
171 |
171 |
172 \begin{center} |
172 \begin{center} |
173 $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ |
173 $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ |
174 \end{center} |
174 \end{center} |
175 |
175 |