nominal2: comparison LMCS-Review

equal deleted inserted replaced

-:4bad521e3b9e
+:8be3155c014f
 > algorithm W [...]."  But there is no analysis in the paper of what was
 > hard in algorithm W coded with single binders, or explanation of how
 > 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
+We have expanded on the point and given details why single
-formalisations.
+binders lead to clumsy formalisations of W.
 > Although this example is
 > one of the main motivations given for the work, there is apparently no
 > formalization of algorithm W in the library of examples that comes
 > with Nominal2 described in this paper.  I think that should be
 > Isabelle and similar theorem provers that only provide mechanisms for
 > binding single variables have not fared extremely well with the more
 > 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.
+We proved the main properties about type-schemes in algorithm W:
-Though the complete formalisation is not yet in place.
+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
 > developers.  This paper would have more impact if interested users
 > 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:
 >
 > Bottom of p.7: I don't understand the paragraph containing equations
 > relation are dropped in the examples, so the examples are not clear.
 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 [...]"
 > Did you mean "({x,y},x->y) and ({y,x},x->y) are alpha-equivalent"?
 >   examples of what
 >   is *forbidden* (with informal explanations why these examples are
 >   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
+for nominal datatypes. Then we would need to think about what to do with
-we have is that we give a sensible "upper bound". To appreciate this point,
+nested datatype, before coming to nominal matters.
-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.
+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
 >   variants of it.) This is good: it makes the whole construction modular
 >   and helps simplify what follows. I don't know if this will make sense
 >   explain/motivate the design of the surface specification language in
 >   terms of these elementary notions, the paper might become all the more
 >   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
+to be as close as possible to what is used in the "wild" (and in Ott).
-us to isolate the notions of shallow, deep and recursive binders.
+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
 >   presented in this paper is still a bit cumbersome: the definitions of free
 >   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).
+the notion of alpha-equivalence for Ott (which has been published). Taking
-So we really of the opinion our definitions are a substantial improvement,
+tgis into account, we really think our definitions are a substantial improvement,
-as witnessed we were actually able to code them up.
+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
 >   atoms outside of their support. But finiteness side conditions seem to
 >   appear pretty early and in unexpected places; e.g. I would expect the
 >   support of a set of atoms "as" to be equal to "as", regardless of whether
 >   "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 = {}
 For sets of atoms the support behaves as follows:
 supp as = as             if as is finite
 supp as = all_atoms      if as and all_atoms - as are infinite
 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
+overkill to include them again in this paper. Since in programming language research
-always only finitely supported structures are of interest, we often restrict
+nearly always considers only finitely supported structures, we often restrict
-to these cases only. Knowing that an object of interest has only finite support
+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,
 >   set, and set+). Perhaps one could make this user-extensible. After
 >   all, very few properties seem to be required of the basic abstraction forms,
 >   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).
+of abstractions (which are different for the set, set+ and list cases).
-So we have not found a unifying framework yet.
+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
 >   standard notion of alpha-equivalence; on the other hand, at the same time,
 >   we take the quotient modulo a notion of structural equivalence (permutation
 >   of binders, removal or introduction of vacuous binders). One could argue
 >   that dealing with structural equivalence should be left to the user, because
 >   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,
+Yes, we can actually only deal with *one* non-trivial structural equivalence,
-namely set+ (introduction of vacuous binders). For us, it seems an application
+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
+from the group around Joachim Parrow are another; in the paper we also point to
-support for set+. Going beyond this is actually quite painful for the user
+work by Altenkirch that uses set+. Therefore we like to give automated support
-if no automatic support is provided.
+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
 >   pair is the same as binding a name within each of the pair components.
 >   (This is the case in first-order logic where forall distributes over
 >   convincing evidence that set and set+ abstractions are useful. (That said,
 >   they don't cost much, so why not include them? Sure.)
 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:
 >
 >     let x1 = t1 and ... and xn = tn in t
 >   of pairs. I think that the system should at the very least allow encoding
 >   this example, otherwise set-abstractions will not be very useful in
 >   practice.
 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,
 > I am not
 > compared
 > with one another. For this reason, it is not clear that a notion of
 > 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
+much sense. This is different from *implementations* of W. They
-might get away with concrete representations of tyep-schemes.
+might get away with concrete representations of type-schemes.
 > p.3, "let the user chose" -> "choose"
 Fixed.
 > Equation (2.2) is unfamiliar to me. I am used to seeing "supp x" defined as
 > the least set L such that for every permutation pi, if pi fixes L, then pi
 > 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,
 to which we refer the reader.
 > intuitively true if we remove this hypothesis: it states exactly that
 > "supp x"
 > 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
 but
 > suggestion, could one decide to expose only Set+ equality to the programmer,
 > and let him/her explicitly encode Set/List equality where desired?
 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
+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
+of set+. Also often proving properties for set+ is harder than for the
-as alpha-equivalence, the encoding, in our opinion, blurrs this difference.
+other modes.
-We noted these facts in the conclusion.
+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"
 Fixed.
 > 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
+Yes, we have this now as the definition. Earlier we really had
-as straightforward in Isabelle - it would need the function package
+derived this. Both methods need equal work (the definition
-and a messy proof that the function is "proper". It is easier to
+needs a proof to be proper). Having it as definition is clearer.
-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.
 > 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
 > an x with infinite support.
 > (binds bn(x) in ...). I would hope that a shallow binder is just syntactic
 > sugar for a deep binder where "bn" is the "singleton list" or "singleton
 > 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
 > exclude "binds bn_1(p) bn_2(p) in t". Couldn't this be accepted and
 > interpreted as "binds bn_1(p) \cup bn_2(p) in t"? (I guess it does not matter
 > p.14, you also exclude "binds bn1(p) in t1, binds bn2(p) in t2". Two
 > questions. First, a clarification: if bn1 and bn2 are the same function, is
 > 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
 > free at the same time" (bound in one sub-term and free in another). I
 > mean, in
 > x in t1 are considered bound, whereas occurrences of x in t2 are considered
 > free; is this correct? If so, why not allow "binds bn1(p) in t1, binds bn2(p)
 > 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
 > is a list of binders, where each binder scopes over the rest of the
 > telescope,
 > explicitly forbidden this situation. So, is it forbidden or allowed? Please
 > clarify.
 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*
 > form (unions of expressions of the form "constant set" or "recursive call").
 > For instance, "rhs" cannot contain the expression "my_empty_set z_i", where

changeset 3129	8be3155c014f
parent 3126	d3d5225f4f24