47 > reasoning, it is not explained in the paper. E.g. on p.1 "However, |
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 |
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 |
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 |
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 |
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 |
52 > the new approach works better in practice. |
|
53 |
|
54 Added |
|
55 |
|
56 > Although this example is |
53 > one of the main motivations given for the work, there is apparently no |
57 > 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 |
58 > formalization of algorithm W in the library of examples that comes |
55 > with Nominal2 described in this paper. I think that should be |
59 > with Nominal2 described in this paper. I think that should be |
56 > provided. Similarly for the second motivating example (on p.2 "The |
60 > provided. Similarly for the second motivating example (on p.2 "The |
57 > need of iterating single binders is also one reason why Nominal |
61 > need of iterating single binders is also one reason why Nominal |
58 > Isabelle and similar theorem provers that only provide mechanisms for |
62 > Isabelle and similar theorem provers that only provide mechanisms for |
59 > binding single variables have not fared extremely well with the more |
63 > binding single variables have not fared extremely well with the more |
60 > advanced tasks in the POPLmark challenge [2], because also there one |
64 > advanced tasks in the POPLmark challenge [2], because also there one |
61 > would like to bind multiple variables at once."). |
65 > would like to bind multiple variables at once."). |
62 > |
66 |
|
67 No time to provide full examples yet. They will be provided |
|
68 once Nominal2 becomes more mature and people are using it |
|
69 and help to provide theories. |
|
70 |
63 > The new Isabelle package "Nominal2", described in this paper, is not |
71 > The new Isabelle package "Nominal2", described in this paper, is not |
64 > ready for users without a lot of hand-holding from the Nominal2 |
72 > ready for users without a lot of hand-holding from the Nominal2 |
65 > developers. This paper would have more impact if interested users |
73 > developers. This paper would have more impact if interested users |
66 > could try the tool without so much difficulty. |
74 > could try the tool without so much difficulty. |
67 > |
75 |
|
76 The plan is to have Nominal Isabelle be part of the next stable |
|
77 release of Isabelle, which should be out before the summer 2012. |
|
78 At the moment it can be downloaded as a bundle and is ready |
|
79 to be used (we have confirmation from two groups for this). |
|
80 |
68 > A few more specific points: |
81 > A few more specific points: |
69 > |
82 > |
70 > Bottom of p.7: I don't understand the paragraph containing equations |
83 > Bottom of p.7: I don't understand the paragraph containing equations |
71 > (2.4) and (2.5). |
84 > (2.4) and (2.5). |
72 > |
85 |
|
86 |
73 > Bottom of p.9: The parameters R and fa of the alpha equivalence |
87 > 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. |
88 > 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 |
89 > 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 [...]" |
90 > 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"? |
91 > Did you mean "({x,y},x->y) and ({y,x},x->y) are alpha-equivalent"? |
78 > |
92 |
79 > |
93 |
|
94 |
80 > Referee no 2: |
95 > Referee no 2: |
81 > |
96 > |
82 > * The paper can be accepted for Logical Methods in Computer Science |
97 > * The paper can be accepted for Logical Methods in Computer Science |
83 > after minor |
98 > after minor |
84 > revisions |
99 > revisions |
186 > might be possible, if one represents the definitions "x1 = t1 and ..." |
201 > 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 |
202 > 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 |
203 > 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 |
204 > this example, otherwise set-abstractions will not be very useful in |
190 > practice. |
205 > practice. |
|
206 |
|
207 >> datatype trm = |
|
208 >> Var string |
|
209 >> | App trm trm |
|
210 >> | Lam string trm |
|
211 >> | Let "(string * trm) fset" trm |
|
212 >> Not a problem. Both finite sets and bags should be possible as |
|
213 >> constructors within the new package. |
|
214 >> Best regards and a happy new year! |
|
215 >> Andrei Popescu |
|
216 |
|
217 |
191 > |
218 > |
192 > Detailed comments |
219 > Detailed comments |
193 > |
220 > |
194 > [Written while I was reading, so sometimes I ask a question whose |
221 > [Written while I was reading, so sometimes I ask a question whose |
195 > answer comes |
222 > answer comes |