|
1 |
|
2 > Referee no 1: |
|
3 > |
|
4 > * The paper can be accepted for Logical Methods in Computer Science |
|
5 > after minor |
|
6 > revisions |
|
7 > |
|
8 > NUMBER : LMCS-2011-675 |
|
9 > TITLE : General Bindings and Alpha-Equivalence in Nominal Isabelle |
|
10 > AUTHOR(S) : Christian Urban, Cezary Kaliszyk |
|
11 > |
|
12 > Recommendation: The paper can be accepted for Logical Methods in |
|
13 > Computer Science after minor revisions. |
|
14 > |
|
15 > The work reported is very good, but the presentation of the paper can |
|
16 > be improved. |
|
17 > |
|
18 > This paper continues a line of work called "Nominal Isabelle" carried |
|
19 > out by the first author and his colleagues for many years. The goal |
|
20 > of this work is to support formal (machine checked) reasoning about |
|
21 > languages with binding. With the theoretical foundation of "nominal |
|
22 > logic" developed by Pitts and colleagues, these authors and their |
|
23 > co-workers have developed a package to support such reasoning in the |
|
24 > Isabelle proof tool for Higher Order Logic. This toolkit has been |
|
25 > widely used, and although the technology sometimes shows through |
|
26 > (e.g. explicit name swapping required in arguments) it is a very good |
|
27 > package. |
|
28 > |
|
29 > Up to now, this package has supported single binders such as \lambda. |
|
30 > Multiple simultaneous binding (e.g. letrec) had to be coded using |
|
31 > iterated single binders. Not only is this coding hard to reason |
|
32 > about, it often isn't a correct representation of the intended |
|
33 > language. This paper describes a new version of the Isabelle package, |
|
34 > "Nominal2", supporting binding of sets and lists of names in the |
|
35 > Isabelle/HOL system. |
|
36 > |
|
37 > The amount of work involved is immense, and the first author |
|
38 > especially has shown real commitment to continuing development of both |
|
39 > theory and working tools. Everything provided in this package is |
|
40 > claimed to be a definitional extension of HOL: no assumptions or |
|
41 > built-in changes to the logic. For all of these reasons, this is very |
|
42 > good work. |
|
43 > |
|
44 > However, I recommend improvement of the presentation of the paper |
|
45 > before it is accepted by LMCS. While the motivation for the work of |
|
46 > this paper is clear to anyone who has tried to formalize such |
|
47 > reasoning, it is not explained in the paper. E.g. on p.1 "However, |
|
48 > Nominal Isabelle has fared less well in a formalisation of the |
|
49 > algorithm W [...]." But there is no analysis in the paper of what was |
|
50 > hard in algorithm W coded with single binders, or explanation of how |
|
51 > it would be done in the new system reported in this paper showing why |
|
52 > the new approach works better in practice. Although this example is |
|
53 > one of the main motivations given for the work, there is apparently no |
|
54 > formalization of algorithm W in the library of examples that comes |
|
55 > with Nominal2 described in this paper. I think that should be |
|
56 > provided. Similarly for the second motivating example (on p.2 "The |
|
57 > need of iterating single binders is also one reason why Nominal |
|
58 > Isabelle and similar theorem provers that only provide mechanisms for |
|
59 > binding single variables have not fared extremely well with the more |
|
60 > advanced tasks in the POPLmark challenge [2], because also there one |
|
61 > would like to bind multiple variables at once."). |
|
62 > |
|
63 > The new Isabelle package "Nominal2", described in this paper, is not |
|
64 > ready for users without a lot of hand-holding from the Nominal2 |
|
65 > developers. This paper would have more impact if interested users |
|
66 > could try the tool without so much difficulty. |
|
67 > |
|
68 > A few more specific points: |
|
69 > |
|
70 > Bottom of p.7: I don't understand the paragraph containing equations |
|
71 > (2.4) and (2.5). |
|
72 > |
|
73 > Bottom of p.9: The parameters R and fa of the alpha equivalence |
|
74 > relation are dropped in the examples, so the examples are not clear. |
|
75 > I think there is a typo in the first example: "It can be easily |
|
76 > checked that ({x,y},x->y) and ({y,x},y->x) are alpha-equivalent [...]" |
|
77 > Did you mean "({x,y},x->y) and ({y,x},x->y) are alpha-equivalent"? |
|
78 > |
|
79 > |
|
80 > Referee no 2: |
|
81 > |
|
82 > * The paper can be accepted for Logical Methods in Computer Science |
|
83 > after minor |
|
84 > revisions |
|
85 > |
|
86 > General comments |
|
87 > |
|
88 > This paper describes a new implementation of the nominal_datatype package |
|
89 > within the Isabelle/HL theorem prover. This implementation is more modular |
|
90 > than previous versions, because it relies on (I think) three non-trivial |
|
91 > independent packages, namely the datatype package, the function package, and |
|
92 > the quotient package. This implementation is also more powerful than previous |
|
93 > versions, because it deals with abstractions that bind multiple names |
|
94 > at once, |
|
95 > and because it offers two variants of these abstractions (baptised "set" and |
|
96 > "set+") where certain structural equivalence laws, namely the exchange of two |
|
97 > binders and the elimination/introduction of a vacuous binder, are built |
|
98 > directly into the alpha-equivalence relation. |
|
99 > |
|
100 > Overall, I like the paper because it describes a useful piece of software, |
|
101 > because the architecture of this software is quite non-trivial and well |
|
102 > designed, and because the paper is written in a very understandable style. |
|
103 > For these reasons, I believe the paper should be accepted. I do have a series |
|
104 > of questions and suggestions for potential improvements and would be happy to |
|
105 > review a revised version of the paper if the editor sees fit. |
|
106 > |
|
107 > My main criticisms of the paper are: |
|
108 > |
|
109 > * The definition of the "nominal signature" language is not completely clear. |
|
110 > The general format at the beginning of section 4 is very clear, but is in |
|
111 > fact too general: not everything that can be written in this format makes |
|
112 > sense. The authors then walk the reader through a series of |
|
113 > examples of what |
|
114 > is *forbidden* (with informal explanations why these examples are |
|
115 > forbidden), but in the end, a positive definition of what is *permitted* |
|
116 > seems to be missing. |
|
117 > |
|
118 > * The authors have isolated an important building block, the notion of |
|
119 > (multiple-name) abstraction (in Section 3). (Actually, there are three |
|
120 > variants of it.) This is good: it makes the whole construction modular |
|
121 > and helps simplify what follows. I don't know if this will make sense |
|
122 > for the authors, but I would like them to go further in this direction: |
|
123 > identify more elementary building blocks ("combinators", if you will), |
|
124 > study their properties in isolation, and in the end combine them to |
|
125 > obtain a very simple explanation of the "nominal signature" format |
|
126 > that is exposed to the user. In the present state of the paper, the |
|
127 > design of the "nominal signature" format seems somewhat ad hoc: the |
|
128 > format of the "binds" clauses is subject to several restrictions; |
|
129 > there seems to be a distinction between "binders" and ordinary |
|
130 > "terms"; there is a distinction between "recursive" and "non-recursive" |
|
131 > binders, and a distinction between "shallow" and "deep" binders. If |
|
132 > one could identify a small number of elementary building blocks and |
|
133 > explain/motivate the design of the surface specification language in |
|
134 > terms of these elementary notions, the paper might become all the more |
|
135 > compelling. |
|
136 > |
|
137 > In the present state of the paper, I think the *implementation* of the |
|
138 > nominal package is very useful for the end user, but the *theory* that is |
|
139 > presented in this paper is still a bit cumbersome: the definitions of free |
|
140 > atoms, alpha-equivalence, etc. presented on pages 16-20 are understandable |
|
141 > but not compelling by their simplicity. |
|
142 > |
|
143 > * I do not quite understand the treatment of the finiteness restriction. |
|
144 > I understand that things must have finite support so as to allow picking |
|
145 > atoms outside of their support. But finiteness side conditions seem to |
|
146 > appear pretty early and in unexpected places; e.g. I would expect the |
|
147 > support of a set of atoms "as" to be equal to "as", regardless of whether |
|
148 > "as" is finite or infinite. This could be clarified. |
|
149 > |
|
150 > * The choice of abstraction "style" is limited to three built-in forms (list, |
|
151 > set, and set+). Perhaps one could make this user-extensible. After |
|
152 > all, very |
|
153 > few properties seem to be required of the basic abstraction forms, |
|
154 > so why not |
|
155 > let the user define new ones? |
|
156 > |
|
157 > * One may argue that the set-abstractions are an attempt to kill two birds |
|
158 > with one stone. On the one hand, we take the quotient raw terms modulo a |
|
159 > standard notion of alpha-equivalence; on the other hand, at the same time, |
|
160 > we take the quotient modulo a notion of structural equivalence (permutation |
|
161 > of binders, removal or introduction of vacuous binders). One could argue |
|
162 > that dealing with structural equivalence should be left to the |
|
163 > user, because |
|
164 > in general the structural equivalence axioms that the user needs can be |
|
165 > arbitrarily complex and application-specific. There are object languages, |
|
166 > for instance, where abstractions commute with pairs: binding a name in a |
|
167 > pair is the same as binding a name within each of the pair components. |
|
168 > (This is the case in first-order logic where forall distributes over |
|
169 > conjunction.) Thus, one may fear that in many cases, the set and set+ |
|
170 > abstractions will not be sufficiently powerful to encode the desired |
|
171 > structural equivalence, and the user will need to explicitly define |
|
172 > a notion |
|
173 > of structural equivalence anyway. I don't think that the paper provides |
|
174 > convincing evidence that set and set+ abstractions are useful. (That said, |
|
175 > they don't cost much, so why not include them? Sure.) |
|
176 > |
|
177 > * Here is little challenge related to set-abstractions. Could you explain how |
|
178 > to define the syntax of an object language with a construct like this: |
|
179 > |
|
180 > let x1 = t1 and ... and xn = tn in t |
|
181 > |
|
182 > where the xi's are bound in t (this is a non-recursive multiple-let form) |
|
183 > and the order of the definitions does not matter (that is, "let x1 = t1 |
|
184 > and x2 = t2 in t" is alpha-equivalent to "let x2 = t2 and x1 = t1 in t")? |
|
185 > Can you use a set-abstraction to achieve this? I am guessing that this |
|
186 > might be possible, if one represents the definitions "x1 = t1 and ..." |
|
187 > using a set of pairs (or a map of names to terms) as opposed to a list |
|
188 > of pairs. I think that the system should at the very least allow encoding |
|
189 > this example, otherwise set-abstractions will not be very useful in |
|
190 > practice. |
|
191 > |
|
192 > Detailed comments |
|
193 > |
|
194 > [Written while I was reading, so sometimes I ask a question whose |
|
195 > answer comes |
|
196 > a bit later in the paper.] |
|
197 > |
|
198 > p.2, "this leads to a rather clumsy formalisation of W". Could you explain |
|
199 > why? Although I can understand why in some circumstances it is desirable to |
|
200 > have a notion of alpha-equivalence that includes re-ordering binders, |
|
201 > I am not |
|
202 > sure that the ML type system (or its inference algorithm) is a good |
|
203 > illustration. If one examines the typing rules of Core ML, one finds that |
|
204 > their premises involve a notion of equality between *types* (for |
|
205 > instance, the |
|
206 > function application rule requires that the types of the formal and actual |
|
207 > arguments match) but do not involve any notion of equality between *type |
|
208 > schemes*. Type schemes are constructed and eliminated; they are never |
|
209 > compared |
|
210 > with one another. For this reason, it is not clear that a notion of |
|
211 > alpha-equivalence for type schemes is required at all, let alone that it must |
|
212 > allow re-ordering binders and/or disregarding vacuous binders. |
|
213 > |
|
214 > p.3, "let the user chose" -> "choose" |
|
215 > |
|
216 > p.5, I am not sure what you mean by "automatic proofs". Do you mean |
|
217 > automatically-generated proof scripts, or proofs performed automatically by a |
|
218 > decision procedure, or ... ? |
|
219 > |
|
220 > p.5, "adaption" |
|
221 > |
|
222 > p.5, it seems strange to use the symbol "+" for composition, a |
|
223 > non-commutative |
|
224 > operation. |
|
225 > |
|
226 > Equation (2.2) is unfamiliar to me. I am used to seeing "supp x" defined as |
|
227 > the least set L such that for every permutation pi, if pi fixes L, then pi |
|
228 > fixes x. I assume that the two definitions are equivalent? Is there a reason |
|
229 > why you prefer this one? |
|
230 > |
|
231 > Proposition 2.3, item (i) is not very easy to read, because text and math |
|
232 > are mixed and "as" happens to be an English word. More importantly, could |
|
233 > you explain why the hypothesis "finite as" is needed? The proposition seems |
|
234 > intuitively true if we remove this hypothesis: it states exactly that |
|
235 > "supp x" |
|
236 > is the least set that supports x (this is actually the definition of "supp" |
|
237 > that I expected, as mentioned above). |
|
238 > |
|
239 > p.8, "equivariant functions have empty support". I suppose the converse is |
|
240 > true, i.e. "functions that have empty support are equivariant". If this is |
|
241 > correct, please say so. |
|
242 > |
|
243 > p.8, "we used extensively Property 2.1". You mean "Proposition 2.1". Perhaps |
|
244 > it would be good to choose distinct numbers for inline equations and for |
|
245 > propositions. |
|
246 > |
|
247 > p.8, "we identify four conditions: (i) [...] x and y need to have the same |
|
248 > set of free atoms". You seem to be saying that fa(x) and fa(y) should be |
|
249 > equal. But this is too strong; I suppose you mean fa(x) \ as = fa(y) \ bs. |
|
250 > Please clarify. (Definition 3.1 indeed clarifies this, but I believe that |
|
251 > the text that precedes it is a bit confusing.) |
|
252 > |
|
253 > p.9, it seems to me that alpha-equivalence for Set+ bindings (Definition 3.3) |
|
254 > is in a sense the most general of the three notions presented here. Indeed, |
|
255 > alpha-equivalence for Set bindings can be defined in terms of it, as follows: |
|
256 > |
|
257 > (as, x) =_{Set} (bs, y) |
|
258 > if and only if |
|
259 > (as, (as, x)) =_{Set+} (bs, (bs, y)) |
|
260 > |
|
261 > That is, I am comparing abstractions whose body has type "atom set * beta". |
|
262 > The comparison of the set components forces condition (iv) of Definition 3.1. |
|
263 > Similarly, alpha-equivalence for List bindings can be defined in terms of it, |
|
264 > as follows: |
|
265 > |
|
266 > (as, x) =_{List} (bs, y) |
|
267 > if and only if |
|
268 > (set as, (as, x)) =_{Set+} (set bs, (bs, y)) |
|
269 > |
|
270 > That is, I am comparing abstractions whose body has type "atom list * beta". |
|
271 > Am I correct to think that one can do this? If so, could this help eliminate |
|
272 > some redundancy in the paper or in the implementation? And, for a |
|
273 > more radical |
|
274 > suggestion, could one decide to expose only Set+ equality to the programmer, |
|
275 > and let him/her explicitly encode Set/List equality where desired? |
|
276 > |
|
277 > p.10, "in these relation" |
|
278 > |
|
279 > p.10, isn't equation (3.3) a *definition* of the action of permutations |
|
280 > on the newly defined quotient type "beta abs_{set}"? |
|
281 > |
|
282 > p.11, why do you need to "assume that x has finite support" in order to |
|
283 > obtain property 3.4? It seems to me that this fact should also hold for |
|
284 > an x with infinite support. Same remark in a couple of places further |
|
285 > down on this page. You note that "supp bs = bs" holds "for every finite |
|
286 > set of atoms bs". Is it *not* the case that this also holds for infinite |
|
287 > sets? If so, what *is* the support of an infinite set of atoms? Why not |
|
288 > adopt a definition of support that validates "supp bs = bs" for *every* |
|
289 > set of atoms bs? Is there a difficulty due to the fact that what you |
|
290 > call a "permutation" is in a fact "a permutation with finite support"? |
|
291 > I think it would be good to motivate your technical choices and clarify |
|
292 > exactly where/why a finite support assumption is required. |
|
293 > |
|
294 > p.11, "The other half is a bit more involved." I would suggest removing |
|
295 > this rather scary sentence. The proof actually appears very simple and |
|
296 > elegant to me. |
|
297 > |
|
298 > p.12, "mutual recursive" -> "mutually recursive" |
|
299 > |
|
300 > p.12, does the tool support parameterized data type definitions? If so, |
|
301 > please mention it, otherwise explain whether there is a difficulty (e.g. |
|
302 > the parameters would need to come with a notion of permutation). |
|
303 > |
|
304 > p.12, "Interestingly, [...] will make a difference [...]". At this |
|
305 > point, upon |
|
306 > first reading, this is not "interesting" but rather frustrating, because it |
|
307 > does not sound natural: my understanding would be very much simplified if |
|
308 > "binds ... in t u" was equivalent to "binds ... in t, binds ... in |
|
309 > u". Because |
|
310 > a forward pointer is missing, I cannot find immediately where this is |
|
311 > explained, and this problem hinders my reading of the beginning of section 5. |
|
312 > |
|
313 > p.13, the type of sets now seems to be "fset" whereas it was "set" |
|
314 > previously. |
|
315 > |
|
316 > p.13, the type of atoms now seems to be "name", whereas it was previously |
|
317 > "atom". The remark on the last line of page 13 leads me to understand that |
|
318 > "name" refers to one specific sort of atoms, whereas "atom" refers to an |
|
319 > atom of any sort (right?). The function "atom" converts one to the other; |
|
320 > but what is its type (is it overloaded?). |
|
321 > |
|
322 > p.13, you distinguish shallow binders (binds x in ...) and deep binders |
|
323 > (binds bn(x) in ...). I would hope that a shallow binder is just syntactic |
|
324 > sugar for a deep binder where "bn" is the "singleton list" or "singleton |
|
325 > set" function. Is this the case? If not, why not? If yes, perhaps you could |
|
326 > remove all mentions to shallow binders in section 5. |
|
327 > |
|
328 > p.14, "we cannot have more than one binding function for a deep binder". You |
|
329 > exclude "binds bn_1(p) bn_2(p) in t". Couldn't this be accepted and |
|
330 > interpreted as "binds bn_1(p) \cup bn_2(p) in t"? (I guess it does not matter |
|
331 > much either way.) |
|
332 > |
|
333 > p.14, you also exclude "binds bn1(p) in t1, binds bn2(p) in t2". Two |
|
334 > questions. First, a clarification: if bn1 and bn2 are the same function, is |
|
335 > this allowed or excluded? Second, I don't understand why you need this |
|
336 > restriction, that is, why you are trying to prevent an atom to be "bound and |
|
337 > free at the same time" (bound in one sub-term and free in another). I |
|
338 > mean, in |
|
339 > the case of single binders, you seem to allow "binds x y in t1, binds |
|
340 > y in t2" |
|
341 > (at least, you have not stated that you disallow this). There, occurrences of |
|
342 > x in t1 are considered bound, whereas occurrences of x in t2 are considered |
|
343 > free; is this correct? If so, why not allow "binds bn1(p) in t1, binds bn2(p) |
|
344 > in t2", which seems to be of a similar nature? Is this a somewhat ad hoc |
|
345 > restriction that simplifies your implementation work, or is there really a |
|
346 > deep reason why accepting this clause would not make sense? |
|
347 > |
|
348 > p.14, example 4.4, the restriction that you impose here seems to rule out |
|
349 > an interesting and potentially useful pattern, namely telescopes. A telescope |
|
350 > is a list of binders, where each binder scopes over the rest of the |
|
351 > telescope, |
|
352 > and in addition all of the names introduced by the telescope are considered |
|
353 > bound by the telescope in some separate term. I am thinking of |
|
354 > something along |
|
355 > the following lines: |
|
356 > |
|
357 > nominal_datatype trm = |
|
358 > | Var name |
|
359 > | Let tele::telescope body::trm binds bn(tele) in body |
|
360 > | ... |
|
361 > |
|
362 > and telescope = |
|
363 > | TNil |
|
364 > | TCons x::name rhs::trm rest::telescope binds x in rest |
|
365 > |
|
366 > binder bn::telescope => atom list |
|
367 > where bn (TNil) = [] |
|
368 > | bn (TCons x rhs rest) = [ atom x ] @ bn(rest) |
|
369 > |
|
370 > You write that "if we would permit bn to return y, then it would not be |
|
371 > respectful and therefore cannot be lifted to alpha-equated lambda-terms". I |
|
372 > can see why there is a problem: if "x" is considered bound (therefore |
|
373 > anonymous) in the telescope "TCons x rhs rest", then it cannot possibly be |
|
374 > returned by a (well-behaved) function "bn". I think that the answer to this |
|
375 > problem should be: we must pick an appropriate notion of alpha-equivalence |
|
376 > for telescopes, and this notion of alpha-equivalence must *not* consider x |
|
377 > as anonymous in "TCons x rhs rest". Instead, x must be considered free in |
|
378 > this telescope. The telescopes "TCons x rhs TNil" and "TCons y rhs TNil" |
|
379 > must be considered distinct. Of course we could achieve this effect just by |
|
380 > removing the clause "binds x in rest", but this would lead to a notion of |
|
381 > alpha-equivalence for "Let" terms which is not the desired one: when writing |
|
382 > "let (x1 = t1; x2 = t2) in t", we would like x1 to be bound in t2, and this |
|
383 > will not be the case if we omit "binds x in rest" in the above definition. |
|
384 > I conclude that your design (which seems very reasonable) cannot currently |
|
385 > express telescopes. It would be nice if you could explicitly discuss this |
|
386 > issue. Is it conceivable that an extension of your system could deal with |
|
387 > telescopes? Other researchers have proposed approaches that can deal with |
|
388 > them (I am thinking e.g. of ``Binders Unbound'' by Weirich et al.). |
|
389 > |
|
390 > Here is another general question. How would you declare a nominal data type |
|
391 > for ML patterns? Informally, the syntax of patterns is: |
|
392 > |
|
393 > p ::= |
|
394 > x (variable) |
|
395 > | (p, p) where bn(p1) and bn(p2) are disjoint (pair) |
|
396 > | (p | p) where bn(p1) = bn(p2) (disjunction) |
|
397 > | ... |
|
398 > |
|
399 > In the case of a pair (or conjunction) pattern, one usually requires that the |
|
400 > two components bind disjoint sets of names, whereas in the case of a |
|
401 > disjunction pattern, one requires that the two components bind exactly the |
|
402 > same sets of names. How would you deal with this? I imagine that one could |
|
403 > just omit these two side conditions in the definition of the nominal data |
|
404 > type, and deal with them separately by defining a well-formedness predicate. |
|
405 > One question: in the definition of the "term" data type, at the point where |
|
406 > one writes "binds bn(p) in t", which variant of the "binds" keyword would one |
|
407 > use: "binds", "binds(set)", or "binds(set+)"? Does it make any difference, |
|
408 > considering that a pattern can have multiple occurrences of a name in binding |
|
409 > position? It would be interesting if you could explain how you would handle |
|
410 > this example. |
|
411 > |
|
412 > Another interesting (perhaps even more tricky) example is the syntax of the |
|
413 > join-calculus. In terms of binding, it is really quite subtle and worth a |
|
414 > look. |
|
415 > |
|
416 > p.15, just before section 5, I note that the completion process does *not* |
|
417 > produce any clause of the form "binds ... in x" (in the Lam case). One could |
|
418 > have expected it to produce "binds x in x", for instance. One could imagine |
|
419 > that, for *every* constructor argument t, there is a clause of the |
|
420 > form "binds |
|
421 > .. in t". Here, you adopt a different approach: you seem to be partitioning |
|
422 > the constructor arguments in two categories, the "terms" (which after |
|
423 > completion appear in the right-hand side of exactly one "binds" clause) and |
|
424 > the "binders" (which appear in the left-hand side of at least one "binds" |
|
425 > clause). Please clarify whether this is indeed the case. (You have |
|
426 > presented a |
|
427 > series of data type definitions that you forbid, but in the end, you should |
|
428 > present a succinct summary of what is allowed.) Also, I seem to understand |
|
429 > that the following definition is forbidden: |
|
430 > |
|
431 > nominal_datatype trm = |
|
432 > | Foo t1::trm t2::trm binds bn(t1) in t2, binds bn(t2) in t1 |
|
433 > |
|
434 > (for some definition of "bn"). This would be forbidden because t1 and t2 are |
|
435 > used both as "terms" and as "binders" (both on the left-hand and right-hand |
|
436 > side of a "binds" clause). As far as I can see, however, you have not |
|
437 > explicitly forbidden this situation. So, is it forbidden or allowed? Please |
|
438 > clarify. |
|
439 > |
|
440 > If there is indeed a partition between "terms" and "binders", please justify |
|
441 > why things must be so. I can think of a more general and more symmetric |
|
442 > approach, where instead of writing "binds bn(p) in t" and considering that "p |
|
443 > is a binder" and "t is a term", one would write "binds bn(p) in p t" and |
|
444 > consider that p and t play a priori symmetric roles: the only difference |
|
445 > between them stems from the fact that we collect the bound names |
|
446 > inside p, but |
|
447 > not inside t. (I am not suggesting that the user should write this, but that |
|
448 > the user syntax could be desugared down to something like this if this makes |
|
449 > the theory simpler.) Ah, but I guess that if one were to follow this path, |
|
450 > then one would need a way of distinguishing recursive versus non-recursive |
|
451 > binders. I guess I see why your design makes sense, but perhaps you should |
|
452 > better explain that it is a compromise between several other possible designs |
|
453 > (``alphacaml'', ``binders unbound'', etc. are examples of other designs) and |
|
454 > how you reached this particular point in the design space. |
|
455 > |
|
456 > OK, now I see that, since you allow ``recursive binders'', there is not a |
|
457 > partition between ``terms'' and ``binders''. A recursive binder appears both |
|
458 > on the left- and right-hand sides of a binds clause. Do you require that it |
|
459 > appears on the left- and right-hand sides of *the same* binds clause, or do |
|
460 > you allow the above example ("binds bn(t1) in t2, binds bn(t2) in t1")? If |
|
461 > you do allow it, then I suppose t1 is viewed as a (non-recursive) binder in |
|
462 > the first clause, while t2 is viewed as a (non-recursive) binder in the |
|
463 > second clause. This would be kind of weird, and (I imagine) will not lead |
|
464 > to a reasonable notion of alpha-equivalence. I am hoping to find out later |
|
465 > in the paper. |
|
466 > |
|
467 > p.17, "we have to add in (5.3) the set [...]". It is not very clear whether |
|
468 > you are suggesting that equation 5.3 is incomplete and something should be |
|
469 > added to it, or equation 5.3 is fine and you are referring to B' which is |
|
470 > there already. I suppose the latter. |
|
471 > |
|
472 > p.17, "for each of the arguments we calculate the free atoms as |
|
473 > follows": this |
|
474 > definition relies on the fact that "rhs" must be of a specific *syntactic* |
|
475 > form (unions of expressions of the form "constant set" or "recursive call"). |
|
476 > For instance, "rhs" cannot contain the expression "my_empty_set z_i", where |
|
477 > "my_empty_set" is a user-defined function that always returns the empty set; |
|
478 > otherwise the third bullet would apply and we would end up considering "z_i" |
|
479 > as neither free nor bound. You have mentioned near the top of page 15 that |
|
480 > binding functions "can only return" certain results. You should clarify that |
|
481 > you are not restricting just *the values* that these functions can |
|
482 > return, but |
|
483 > the *syntactic form* of these functions. |
|
484 > |
|
485 > p.23, "We call these conditions as": not really grammatical. |
|
486 > |
|
487 > p.23, "cases lemmas": I suppose this means an elimination principle? |
|
488 > |
|
489 > p.23, "Note that for the term constructors" -> "constructor" |
|
490 > |
|
491 > p.26, "avoid, or being fresh for" -> "avoid, or are fresh for" |
|
492 > |
|
493 > p.30, "Second, it covers cases of binders depending on other binders, |
|
494 > which just do no not make sense [...]". I am curious why the designers |
|
495 > of Ott thought that these cases make sense and you don't. Perhaps this |
|
496 > point would deserve an example and a deeper discussion? |
|
497 > |
|
498 > p.30, at last, here is the discussion of "binds ... in s t" versus |
|
499 > "binds ... in s, binds ... in t". I see that the difference in the |
|
500 > two interpretations boils down to an abstraction whose body is a pair, |
|
501 > versus a pair of abstractions. It is indeed interesting to note that |
|
502 > these notions coincide for single-name abstractions, and for list |
|
503 > abstractions, but not for set and set+ abstractions. |
|
504 > |
|
505 > p.32, "It remains to be seen whether properties like [...] allow us |
|
506 > to support more interesting binding functions." Could you clarify |
|
507 > what you mean? Do you mean (perhaps) that fa_bn(x) could be defined |
|
508 > as fa_ty(x) \ bn(x), regardless of the definition of bn(x), instead |
|
509 > of by induction over x? Do you mean something else? |
|
510 > |
|
511 > The example in Figures 1 and 2 do not seem very interesting to me. It |
|
512 > involves single binders and flat lists of binders. Not much subtlety going on |
|
513 > here. I think this example could be reduced in size without losing |
|
514 > anything in |
|
515 > terms of content. And perhaps a trickier example could be added (I have two |
|
516 > suggestions, which I mentioned above already: ML with conjunction and |
|
517 > disjunction patterns; and the join-calculus). |
|
518 > |
|
519 > |
|
520 > |
|
521 > |
|
522 > |
|
523 > |
|
524 > |
|
525 |