diff -r 4bad521e3b9e -r 8be3155c014f LMCS-Review --- a/LMCS-Review Wed Feb 29 04:56:06 2012 +0000 +++ b/LMCS-Review Wed Feb 29 16:23:11 2012 +0000 @@ -27,8 +27,8 @@ > it would be done in the new system reported in this paper showing why > the new approach works better in practice. -We have expanded on the point why single binders lead to clumsy -formalisations. +We have expanded on the point and given details why single +binders lead to clumsy formalisations of W. > Although this example is > one of the main motivations given for the work, there is apparently no @@ -41,8 +41,9 @@ > advanced tasks in the POPLmark challenge [2], because also there one > would like to bind multiple variables at once."). -We proved the main properties about type-schemes in algorithm W. -Though the complete formalisation is not yet in place. +We proved the main properties about type-schemes in algorithm W: +the ones that caused problems in our earlier formalisation. Though +the complete formalisation of W is not yet in place. > The new Isabelle package "Nominal2", described in this paper, is not > ready for users without a lot of hand-holding from the Nominal2 @@ -50,9 +51,9 @@ > could try the tool without so much difficulty. The plan is to have Nominal Isabelle be part of the next stable -release of Isabelle, which should be out in the summer 2012. +release of Isabelle, which should be out in Autumn 2012. At the moment it can be downloaded as a bundle and is ready -to be used (there are two groups that already use Nominal2 and +to be used (there are two groups that use Nominal2 and only occasionally ask questions on the mailing list). > A few more specific points: @@ -68,7 +69,7 @@ We have two minds with this: Keeping R and fa is more faithful to the definition, but it would not provide much intuition into the definition. We feel explaining the definition in special -cases is most beneficial to the reader. +cases is more beneficial to the reader. > I think there is a typo in the first example: "It can be easily > checked that ({x,y},x->y) and ({y,x},y->x) are alpha-equivalent [...]" @@ -92,13 +93,16 @@ > forbidden), but in the end, a positive definition of what is *permitted* > seems to be missing. -Yes, we agree very much, a positive definition would be very desirable. +Yes, we agree very much: a positive definition would be very desirable. Unfortunately, this is not as easy as one would hope. Already a positive definition for a *datatype* in HOL is rather tricky. We would rely on this -for nominal datatypes. The only real defence for not giving a positive -we have is that we give a sensible "upper bound". To appreciate this point, -you need to consider that systems like Ott go beyond this upper bound and -give definitions which are not sensible as (named) alpha-equated structures. +for nominal datatypes. Then we would need to think about what to do with +nested datatype, before coming to nominal matters. + +The only real defence for not giving a positive we have is that we give a +sensible "upper bound". To appreciate this point, you need to consider that +systems like Ott go beyond this upper bound and give definitions which are +not sensible in the context of (named) alpha-equated structures. > * The authors have isolated an important building block, the notion of > (multiple-name) abstraction (in Section 3). (Actually, there are three @@ -120,11 +124,11 @@ > compelling. We are not sure whether we can make progress with this. There is such a -"combinator approach" described by Francois Pottier for C\alphaML. His approach +"combinator approach" described by Francois Pottier for C-alpha-ML. His approach only needs an inner and outer combinator. However, this has led to quite non-intuitive representations of "nominal datatypes". We attempted -to be as close as possible to what is used in the "wild". This led -us to isolate the notions of shallow, deep and recursive binders. +to be as close as possible to what is used in the "wild" (and in Ott). +This led us to isolate the notions of shallow, deep and recursive binders. > In the present state of the paper, I think the *implementation* of the > nominal package is very useful for the end user, but the *theory* that is @@ -132,11 +136,11 @@ > atoms, alpha-equivalence, etc. presented on pages 16-20 are understandable > but not compelling by their simplicity. -We agree - simpler would be much better. We refer the referee to "competing" +We agree - simpler would be much better. However, we refer the referee to "competing" definitions that are substantially more complicated. Please try to understand -the notion of alpha-equivalence for Ott (which is published in he literature). -So we really of the opinion our definitions are a substantial improvement, -as witnessed we were actually able to code them up. +the notion of alpha-equivalence for Ott (which has been published). Taking +tgis into account, we really think our definitions are a substantial improvement, +as witnessed by the fact that we were actually able to code them up. > * I do not quite understand the treatment of the finiteness restriction. > I understand that things must have finite support so as to allow picking @@ -146,7 +150,7 @@ > "as" is finite or infinite. This could be clarified. This is a peculiarity of support which has been explained elsewhere in the nominal -literature. Assume all_atoms is the set of all atoms then +literature (pointers in the paper). Assume all_atoms is the set of all atoms then supp all_atoms = {} @@ -157,9 +161,9 @@ supp as = all_atoms - as if as is co-finite As said, such properties have been described in the literature and it would be -overkill to include them again. Since in programming language research nearly -always only finitely supported structures are of interest, we often restrict -to these cases only. Knowing that an object of interest has only finite support +overkill to include them again in this paper. Since in programming language research +nearly always considers only finitely supported structures, we often restrict +our work to these cases. Knowing that an object of interest has only finite support is needed when fresh atoms need to be chosen. > * The choice of abstraction "style" is limited to three built-in forms (list, @@ -168,8 +172,8 @@ > so why not let the user define new ones? This would be nice, but we do make use of the equality properties -of abstractions (which are different in the set, set+ and list case). -So we have not found a unifying framework yet. +of abstractions (which are different for the set, set+ and list cases). +So we have yet to find a unifying framework. > * One may argue that the set-abstractions are an attempt to kill two birds > with one stone. On the one hand, we take the quotient raw terms modulo a @@ -180,12 +184,12 @@ > in general the structural equivalence axioms that the user needs can be > arbitrarily complex and application-specific. -Yes, we can actually only deal with one non-trivial structural equivalence, -namely set+ (introduction of vacuous binders). For us, it seems an application +Yes, we can actually only deal with *one* non-trivial structural equivalence, +namely set+ (introduction of vacuous binders). For us, it seems this is an application that occurs more often than not. Type-schemes are one example; the Psi-calculus -from the group around Joachim Parrow are another. So we like to give automated -support for set+. Going beyond this is actually quite painful for the user -if no automatic support is provided. +from the group around Joachim Parrow are another; in the paper we also point to +work by Altenkirch that uses set+. Therefore we like to give automated support +for set+. Doing this without automatic support would be quite painful for the user. > There are object languages, > for instance, where abstractions commute with pairs: binding a name in a @@ -201,7 +205,7 @@ From our experience, once a feature is included, applications will be found. Case in point, the set+ binder arises naturally in the -psi-calculus. +psi-calculus and is used in work by Altenkirch. > * Here is little challenge related to set-abstractions. Could you explain how > to define the syntax of an object language with a construct like this: @@ -220,7 +224,6 @@ We can. We added this as an example in the conclusion section. - > p.2, "this leads to a rather clumsy formalisation of W". Could you explain > why? Although I can understand why in some circumstances it is desirable to > have a notion of alpha-equivalence that includes re-ordering binders, @@ -237,11 +240,11 @@ > alpha-equivalence for type schemes is required at all, let alone that it must > allow re-ordering binders and/or disregarding vacuous binders. -In the correctness proof of W, the notion of capture-avoiding +In the correctness *proof* of W, the notion of capture-avoiding substitution plays a crucial role. The notion of capture-avoiding substitution without the notion of alpha-equivalence does not make -any sense. This is different from *implementations* of W. They -might get away with concrete representations of tyep-schemes. +much sense. This is different from *implementations* of W. They +might get away with concrete representations of type-schemes. > p.3, "let the user chose" -> "choose" @@ -269,11 +272,11 @@ > fixes x. I assume that the two definitions are equivalent? Is there a reason > why you prefer this one? -Our definition is equivalent to yours for finite supported x. +Our definition is equivalent to yours for finitely supported x. The advantage of our definition is that can be easily stated in a theorem prover since it fits into the scheme - lhs = rhs + constant args = term Your definition as the least set...does not fit into this simple scheme. Our definition has been described extensively elsewhere, @@ -291,7 +294,7 @@ > is the least set that supports x (this is actually the definition of "supp" > that I expected, as mentioned above). -It does not work for non-finitely supported sets of atoms. Imagine +It does *not* work for non-finitely supported sets of atoms. Imagine bs is the set of "even" atoms (a set that is not finite nor co-finite). bs supports bs @@ -344,10 +347,12 @@ The second property holds outright. The first holds provided as and bs are finite sets of atoms. However, we seem to not gain much code reduction -from these properties, except for defining the modes Set and List in terms -of Set+. But since they are three different modes and they behave differently -as alpha-equivalence, the encoding, in our opinion, blurrs this difference. -We noted these facts in the conclusion. +from these properties, except for defining the modes set and list in terms +of set+. Also often proving properties for set+ is harder than for the +other modes. + +Since these modes behave differently as alpha-equivalence, the encoding would, +in our opinion, blurr this difference. We however noted these facts in the conclusion. > p.10, "in these relation" @@ -356,12 +361,9 @@ > p.10, isn't equation (3.3) a *definition* of the action of permutations > on the newly defined quotient type "beta abs_{set}"? -Yes, in principle this could be given as the definition. Unfortunately, this is not -as straightforward in Isabelle - it would need the function package -and a messy proof that the function is "proper". It is easier to -define permutation on abstractions as the lifted version of the permutation -on pairs, and then derive (with the support of the quotient package) that -(3.3) holds. +Yes, we have this now as the definition. Earlier we really had +derived this. Both methods need equal work (the definition +needs a proof to be proper). Having it as definition is clearer. > p.11, why do you need to "assume that x has finite support" in order to > obtain property 3.4? It seems to me that this fact should also hold for @@ -433,7 +435,7 @@ > set" function. Is this the case? If not, why not? If yes, perhaps you could > remove all mentions to shallow binders in section 5. -No, quite. A deep binder can be recursive, which is a notion +Not quite. A deep binder can be recursive, which is a notion that does not make sense for shallow binders. > p.14, "we cannot have more than one binding function for a deep binder". You @@ -448,7 +450,7 @@ > this allowed or excluded? For practical purposes, this is excluded. But the theory would -support this case. +support this case. I added a comment in the paper. > Second, I don't understand why you need this > restriction, that is, why you are trying to prevent an atom to be "bound and @@ -462,7 +464,7 @@ > in t2", which seems to be of a similar nature? The problem is that bn1 and bn2 can pick out different atoms to -be free and bound in p. This requires to exclude this case. +be free and bound in p. Therefore we have to exclude this case. > p.14, example 4.4, the restriction that you impose here seems to rule out > an interesting and potentially useful pattern, namely telescopes. A telescope @@ -566,17 +568,6 @@ It is disallowed. We clarified the text. -> OK, now I see that, since you allow ``recursive binders'', there is not a -> partition between ``terms'' and ``binders''. A recursive binder appears both -> on the left- and right-hand sides of a binds clause. Do you require that it -> appears on the left- and right-hand sides of *the same* binds clause, or do -> you allow the above example ("binds bn(t1) in t2, binds bn(t2) in t1")? If -> you do allow it, then I suppose t1 is viewed as a (non-recursive) binder in -> the first clause, while t2 is viewed as a (non-recursive) binder in the -> second clause. This would be kind of weird, and (I imagine) will not lead -> to a reasonable notion of alpha-equivalence. I am hoping to find out later -> in the paper. - > p.17, "for each of the arguments we calculate the free atoms as > follows": this > definition relies on the fact that "rhs" must be of a specific *syntactic*