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 |
53 more advanced tasks in the POPLmark challenge \cite{challenge05}, because |
53 more advanced tasks in the POPLmark challenge \cite{challenge05}, because |
54 also there one would like to bind multiple variables at once. |
54 also there one would like to bind multiple variables at once. |
55 |
55 |
56 Binding multiple variables has interesting properties that cannot be captured |
56 Binding multiple variables has interesting properties that cannot be captured |
57 easily by iterating single binders. For example in the case of type-schemes we do not |
57 easily by iterating single binders. For example in case of type-schemes we do not |
58 like to make a distinction about the order of the bound variables. Therefore |
58 want to make a distinction about the order of the bound variables. Therefore |
59 we would like to regard the following two type-schemes as alpha-equivalent |
59 we would like to regard the following two type-schemes as alpha-equivalent |
60 % |
60 % |
61 \begin{equation}\label{ex1} |
61 \begin{equation}\label{ex1} |
62 \forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x |
62 \forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x |
63 \end{equation} |
63 \end{equation} |
64 |
64 |
65 \noindent |
65 \noindent |
66 but the following two should \emph{not} be alpha-equivalent |
66 but assuming that $x$, $y$ and $z$ are distinct variables, |
|
67 the following two should \emph{not} be alpha-equivalent |
67 % |
68 % |
68 \begin{equation}\label{ex2} |
69 \begin{equation}\label{ex2} |
69 \forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z |
70 \forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z |
70 \end{equation} |
71 \end{equation} |
71 |
72 |
72 \noindent |
73 \noindent |
73 assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as |
74 Moreover, we like to regard type-schemes as |
74 alpha-equivalent, if they differ only on \emph{vacuous} binders, such as |
75 alpha-equivalent, if they differ only on \emph{vacuous} binders, such as |
75 % |
76 % |
76 \begin{equation}\label{ex3} |
77 \begin{equation}\label{ex3} |
77 \forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y |
78 \forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y |
78 \end{equation} |
79 \end{equation} |
85 for alpha-equivalence in this case can be appreciated by considering that the |
86 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). |
87 definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
87 |
88 |
88 However, the notion of alpha-equivalence that is preserved by vacuous binders is not |
89 However, the notion of alpha-equivalence that is preserved by vacuous binders is not |
89 always wanted. For example in terms like |
90 always wanted. For example in terms like |
90 |
91 % |
91 \begin{equation}\label{one} |
92 \begin{equation}\label{one} |
92 \LET x = 3 \AND y = 2 \IN x\,-\,y \END |
93 \LET x = 3 \AND y = 2 \IN x\,-\,y \END |
93 \end{equation} |
94 \end{equation} |
94 |
95 |
95 \noindent |
96 \noindent |
96 we might not care in which order the assignments $x = 3$ and $y = 2$ are |
97 we might not care in which order the assignments $x = 3$ and $y = 2$ are |
97 given, but it would be unusual to regard \eqref{one} as alpha-equivalent |
98 given, but it would be unusual to regard \eqref{one} as alpha-equivalent |
98 with |
99 with |
99 |
100 % |
100 \begin{center} |
101 \begin{center} |
101 $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$ |
102 $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$ |
102 \end{center} |
103 \end{center} |
103 |
104 |
104 \noindent |
105 \noindent |
107 binders has to agree. |
108 binders has to agree. |
108 |
109 |
109 However, we found that this is still not sufficient for dealing with |
110 However, we found that this is still not sufficient for dealing with |
110 language constructs frequently occurring in programming language |
111 language constructs frequently occurring in programming language |
111 research. For example in $\mathtt{let}$s containing patterns |
112 research. For example in $\mathtt{let}$s containing patterns |
112 |
113 % |
113 \begin{equation}\label{two} |
114 \begin{equation}\label{two} |
114 \LET (x, y) = (3, 2) \IN x\,-\,y \END |
115 \LET (x, y) = (3, 2) \IN x\,-\,y \END |
115 \end{equation} |
116 \end{equation} |
116 |
117 |
117 \noindent |
118 \noindent |
118 we want to bind all variables from the pattern inside the body of the |
119 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 |
120 $\mathtt{let}$, but we also care about the order of these variables, since |
120 we do not want to regard \eqref{two} as alpha-equivalent with |
121 we do not want to regard \eqref{two} as alpha-equivalent with |
121 |
122 % |
122 \begin{center} |
123 \begin{center} |
123 $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ |
124 $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ |
124 \end{center} |
125 \end{center} |
125 |
126 |
126 \noindent |
127 \noindent |
129 programming language calculus. |
130 programming language calculus. |
130 |
131 |
131 By providing these general binding mechanisms, however, we have to work around |
132 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 |
133 a problem that has been pointed out by Pottier in \cite{Pottier06}: in |
133 $\mathtt{let}$-constructs of the form |
134 $\mathtt{let}$-constructs of the form |
134 |
135 % |
135 \begin{center} |
136 \begin{center} |
136 $\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$ |
137 \end{center} |
138 \end{center} |
138 |
139 |
139 \noindent |
140 \noindent |
140 which bind all the $x_i$ in $s$, 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 |
141 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 |
142 as many $x_i$ as there are $t_i$. We lose this information if we represent the |
143 as many $x_i$ as there are $t_i$. We lose this information if we represent the |
143 $\mathtt{let}$-constructor by something like |
144 $\mathtt{let}$-constructor by something like |
144 |
145 % |
145 \begin{center} |
146 \begin{center} |
146 $\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]$ |
147 \end{center} |
148 \end{center} |
148 |
149 |
149 \noindent |
150 \noindent |
152 would be a perfectly legal instance. To exclude such terms an additional |
153 would be a perfectly legal instance. To exclude such terms an additional |
153 predicate about well-formed terms is needed in order to ensure that the two |
154 predicate about well-formed terms is needed in order to ensure that the two |
154 lists are of equal length. This can result into very messy reasoning (see |
155 lists are of equal length. This can result into very messy reasoning (see |
155 for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications |
156 for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications |
156 for $\mathtt{let}$s as follows |
157 for $\mathtt{let}$s as follows |
157 |
158 % |
158 \begin{center} |
159 \begin{center} |
159 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
160 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
160 $trm$ & $::=$ & \ldots\\ |
161 $trm$ & $::=$ & \ldots\\ |
161 & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] |
162 & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] |
162 $assn$ & $::=$ & $\mathtt{anil}$\\ |
163 $assn$ & $::=$ & $\mathtt{anil}$\\ |
383 |
384 |
384 |
385 |
385 section {* General Binders *} |
386 section {* General Binders *} |
386 |
387 |
387 text {* |
388 text {* |
388 In Nominal Isabelle the user is expected to write down a specification of a |
389 In Nominal Isabelle, the user is expected to write down a specification of a |
389 term-calculus and a reasoning infrastructure is then automatically derived |
390 term-calculus and then a reasoning infrastructure is automatically derived |
390 from this specifcation (remember that Nominal Isabelle is a definitional |
391 from this specifcation (remember that Nominal Isabelle is a definitional |
391 extension of Isabelle/HOL and cannot introduce new axioms). |
392 extension of Isabelle/HOL, which does not introduce any new axioms). |
392 |
393 |
393 |
394 |
394 In order to keep our work manageable, we will wherever possible state |
395 In order to keep our work manageable, we will wherever possible state |
395 definitions and perform proofs inside Isabelle, as opposed to write custom |
396 definitions and perform proofs inside Isabelle, as opposed to write custom |
396 ML-code that generates them for each instance of a term-calculus. To that |
397 ML-code that generates them for each instance of a term-calculus. To that |
506 \end{lemma} |
507 \end{lemma} |
507 |
508 |
508 \begin{proof} |
509 \begin{proof} |
509 All properties are by unfolding the definitions and simple calculations. |
510 All properties are by unfolding the definitions and simple calculations. |
510 \end{proof} |
511 \end{proof} |
|
512 |
|
513 |
|
514 \begin{lemma} |
|
515 $supp ([as]set. x) = supp x - as$ |
|
516 \end{lemma} |
511 *} |
517 *} |
512 |
518 |
513 section {* Alpha-Equivalence and Free Variables *} |
519 section {* Alpha-Equivalence and Free Variables *} |
|
520 |
|
521 text {* |
|
522 A specification of a term-calculus in Nominal Isabelle is a collection |
|
523 of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ |
|
524 written as follows: |
|
525 |
|
526 \begin{center} |
|
527 \begin{tabular}{l} |
|
528 \isacommand{nominal\_datatype} $ty_1 =$\\ |
|
529 \isacommand{and} $ty_2 =$\\ |
|
530 $\ldots$\\ |
|
531 \isacommand{and} $ty_n =$\\ |
|
532 $\ldots$\\ |
|
533 \isacommand{with}\\ |
|
534 $\ldots$\\ |
|
535 \end{tabular} |
|
536 \end{center} |
|
537 |
|
538 \noindent |
|
539 The section below the \isacommand{with} are binding functions, which |
|
540 will be explained below. |
|
541 |
|
542 |
|
543 |
|
544 A specification of a term-calculus in Nominal Isabell is very similar to |
|
545 the usual datatype definition of Isabelle/HOL: |
|
546 |
|
547 |
|
548 Because of the problem Pottier pointed out in \cite{Pottier06}, the general |
|
549 binders from the previous section cannot be used directly to represent w |
|
550 be used directly |
|
551 *} |
|
552 |
|
553 |
514 |
554 |
515 text {* |
555 text {* |
516 Restrictions |
556 Restrictions |
517 |
557 |
518 \begin{itemize} |
558 \begin{itemize} |