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