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 where free and bound variables have names. |
26 where free and bound variables have names. For such terms Nominal Isabelle |
27 For such terms Nominal Isabelle derives automatically a reasoning |
27 derives automatically a reasoning infrastructure, which has been used |
28 infrastructure, which has been used successfully in formalisations of an equivalence |
28 successfully in formalisations of an equivalence checking algorithm for LF |
29 checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed |
29 \cite{UrbanCheneyBerghofer08}, Typed |
30 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
30 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
31 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result |
31 \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result |
32 for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been |
32 for cut-elimination in classical logic \cite{UrbanZhu08}. It has also been |
33 used by Pollack for formalisations in the locally-nameless approach to |
33 used by Pollack for formalisations in the locally-nameless approach to |
34 binding \cite{SatoPollack10}. |
34 binding \cite{SatoPollack10}. |
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 type-variables. |
47 and the quantification binds at once a finite (possibly empty) set of |
48 While it is possible to implement this kind of more general binders by iterating single binders, |
48 type-variables. While it is possible to implement this kind of more general |
49 this leads to a rather clumsy formalisation of W. The need of iterating single binders |
49 binders by iterating single binders, this leads to a rather clumsy |
50 is also one reason why Nominal Isabelle and similar |
50 formalisation of W. The need of iterating single binders is also one reason |
51 theorem provers have not fared extremely well with the more advanced tasks |
51 why Nominal Isabelle and similar theorem provers that only provide |
52 in the POPLmark challenge \cite{challenge05}, because also there one would like |
52 mechanisms for binding single variables have not fared extremely well with the |
53 to bind multiple variables at once. |
53 more advanced tasks in the POPLmark challenge \cite{challenge05}, because |
54 |
54 also there one would like to bind multiple variables at once. |
55 Binding multiple variables has interesting properties that are not |
55 |
56 captured by iterating single binders. First, |
56 Binding multiple variables has interesting properties that are not captured |
57 in the case of type-schemes, we do not like to make a distinction |
57 by iterating single binders. First, in the case of type-schemes, we do not |
58 about the order of the bound variables. Therefore we would like to regard the following two |
58 like to make a distinction about the order of the bound variables. Therefore |
59 type-schemes as alpha-equivalent |
59 we would like to regard the following two type-schemes as alpha-equivalent |
60 |
60 |
61 \begin{center} |
61 \begin{center} |
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{center} |
63 \end{center} |
64 |
64 |
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 alway 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\,\backslash\,y \END |
92 \LET x = 3 \AND y = 2 \IN x\,-\,y \END |
93 \end{equation} |
93 \end{equation} |
94 |
94 |
95 \noindent |
95 \noindent |
96 we might not care in which order the assignments $x = 3$ and $y = 2$ are |
96 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 |
97 given, but it would be unusual to regard \eqref{one} as alpha-equivalent |
98 with |
98 with |
99 |
99 |
100 \begin{center} |
100 \begin{center} |
101 $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,\backslash\,y \END$ |
101 $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$ |
102 \end{center} |
102 \end{center} |
103 |
103 |
104 \noindent |
104 \noindent |
105 Therefore we will also provide a separate binding mechanism for cases |
105 Therefore we will also provide a separate binding mechanism for cases in |
106 in which the order of binders does not matter, but the ``cardinality'' of the |
106 which the order of binders does not matter, but the ``cardinality'' of the |
107 binders has to agree. |
107 binders has to agree. |
108 |
108 |
109 However, we found that this is still not sufficient for dealing with language |
109 However, we found that this is still not sufficient for dealing with |
110 constructs frequently occurring in programming language research. For example |
110 language constructs frequently occurring in programming language |
111 in $\mathtt{let}$s involving patterns |
111 research. For example in $\mathtt{let}$s containing patterns |
112 |
112 |
113 \begin{equation}\label{two} |
113 \begin{equation}\label{two} |
114 \LET (x, y) = (3, 2) \IN x\,\backslash\,y \END |
114 \LET (x, y) = (3, 2) \IN x\,-\,y \END |
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 identify \eqref{two} with |
121 |
121 |
122 \begin{center} |
122 \begin{center} |
123 $\LET (y, x) = (3, 2) \IN x\,\backslash 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 we let the user chose which one is intended when formalising a |
138 |
138 |
139 \noindent |
139 \noindent |
140 which bind all the $x_i$ in $s$, we might not care about the order in |
140 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 |
141 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 |
142 as many $x_i$ as there are $t_i$. We lose this information if we represent the |
143 $\mathtt{let}$-constructor as something like |
143 $\mathtt{let}$-constructor by something like |
144 |
144 |
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 |
151 bound in $s$. In this representation we need additional predicates about terms |
151 bound 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 to ensure that the two lists are of equal length. This can result into very |
153 to ensure that the two lists are of equal length. This can result into very |
153 unintelligible reasoning (see for example~\cite{BengtsonParow09}). |
154 messy reasoning (see for example~\cite{BengtsonParow09}). |
154 To avoid this, we will allow to specify $\mathtt{let}$s |
155 To avoid this, we will allow for example to specify $\mathtt{let}$s |
155 as follows |
156 as follows |
156 |
157 |
157 \begin{center} |
158 \begin{center} |
158 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
159 \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} |
159 $trm$ & $::=$ & \ldots\\ |
160 $trm$ & $::=$ & \ldots\\ |
171 \begin{center} |
172 \begin{center} |
172 $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)$ |
173 \end{center} |
174 \end{center} |
174 |
175 |
175 \noindent |
176 \noindent |
176 The scope of the binding is indicated by labels given to the types, for example |
177 The scope of the binding is indicated by labels given to the types, for |
177 $s\!::\!trm$, and a binding clause $\mathtt{bind}\;bn\,(a) \IN s$. |
178 example \mbox{$s\!::\!trm$}, and a binding clause, in this case |
178 This style of specifying terms and bindings is heavily |
179 $\mathtt{bind}\;bn\,(a) \IN s$, that states bind all the names the function |
|
180 $bn$ returns in $s$. This style of specifying terms and bindings is heavily |
179 inspired by the syntax of the Ott-tool \cite{ott-jfp}. |
181 inspired by the syntax of the Ott-tool \cite{ott-jfp}. |
180 |
182 |
181 However, we will not be able to deal with all specifications that are |
183 However, we will not be able to deal with all specifications that are |
182 allowed by Ott. One reason is that we establish the reasoning infrastructure |
184 allowed by Ott. One reason is that we establish the reasoning infrastructure |
183 for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of |
185 for alpha-\emph{equated} terms. In contrast, Ott produces for a subset of |
184 its specifications a reasoning infrastructure in Isabelle for |
186 its specifications a reasoning infrastructure in Isabelle/HOL for |
185 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms |
187 \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms |
186 and the concrete terms produced by Ott use names for the bound variables, |
188 and the raw terms produced by Ott use names for the bound variables, |
187 there is a key difference: working with alpha-equated terms means that the |
189 there is a key difference: working with alpha-equated terms means that the |
188 two type-schemes with $x$, $y$ and $z$ being distinct |
190 two type-schemes with $x$, $y$ and $z$ being distinct |
189 |
191 |
190 \begin{center} |
192 \begin{center} |
191 $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ |
193 $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ |
192 \end{center} |
194 \end{center} |
193 |
195 |
194 \noindent |
196 \noindent |
195 are not just alpha-equal, but actually equal (note the ``=''-sign). Our insistence |
197 are not just alpha-equal, but actually equal. As a |
196 on reasoning with alpha-equated terms comes from the wealth of experience we gained with |
198 result, we can only support specifications that make sense on the level of |
197 the older version of Nominal Isabelle: for non-trivial properties, reasoning |
199 alpha-equated terms (offending specifications, which for example bind a variable |
198 about alpha-equated terms is much easier than reasoning with concrete |
200 according to a variable bound somewhere else, are not excluded by Ott). Our |
199 terms. The fundamental reason is that the HOL-logic underlying |
201 insistence on reasoning with alpha-equated terms comes from the wealth of |
200 Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast replacing |
202 experience we gained with the older version of Nominal Isabelle: for |
201 ``alpha-equals-by-alpha-equals'' in a term calculus requires a lot of extra reasoning work. |
203 non-trivial properties, reasoning about alpha-equated terms is much easier |
202 |
204 than reasoning with raw terms. The fundamental reason is that the |
203 |
205 HOL-logic underlying Nominal Isabelle allows us to replace |
|
206 ``equals-by-equals''. In contrast replacing ``alpha-equals-by-alpha-equals'' |
|
207 in a representation based on raw terms requires a lot of extra reasoning work. |
|
208 |
204 Although in informal settings a reasoning infrastructure for alpha-equated |
209 Although in informal settings a reasoning infrastructure for alpha-equated |
205 terms (that have names for bound variables) is nearly always taken for granted, establishing |
210 terms (that have names for bound variables) is nearly always taken for granted, establishing |
206 it automatically in a theorem prover is a rather non-trivial task. |
211 it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. |
207 For every specification we will need to construct a type containing as |
212 For every specification we will need to construct a type containing as |
208 elements the alpha-equated terms. To do so we use |
213 elements the alpha-equated terms. To do so we use |
209 the standard HOL-technique of defining a new type by |
214 the standard HOL-technique of defining a new type by |
210 identifying a non-empty subset of an existing type. In our |
215 identifying a non-empty subset of an existing type. In our |
211 case we take as the starting point the type of sets of concrete |
216 case we take as the starting point the type of sets of raw |
212 terms (the latter being defined as a datatype). Then identify the |
217 terms (the latter being defined as a datatype); identify the |
213 alpha-equivalence classes according to our alpha-equivalence relation and |
218 alpha-equivalence classes according to our alpha-equivalence relation and |
214 then identify the new type as these alpha-equivalence classes. The construction we |
219 then define the new type as these alpha-equivalence classes. The construction we |
215 can perform in HOL is illustrated by the following picture: |
220 can perform in HOL is illustrated by the following picture: |
216 |
221 |
217 \begin{center} |
222 \begin{center} |
218 figure |
223 figure |
219 %\begin{pspicture}(0.5,0.0)(8,2.5) |
224 %\begin{pspicture}(0.5,0.0)(8,2.5) |