diff -r 860df8e1262f -r d3d5225f4f24 LMCS-Review
--- a/LMCS-Review Wed Feb 22 12:10:17 2012 +0000
+++ b/LMCS-Review Wed Feb 29 03:12:52 2012 +0000
@@ -15,31 +15,7 @@
> The work reported is very good, but the presentation of the paper can
> be improved.
>
-> This paper continues a line of work called "Nominal Isabelle" carried
-> out by the first author and his colleagues for many years. The goal
-> of this work is to support formal (machine checked) reasoning about
-> languages with binding. With the theoretical foundation of "nominal
-> logic" developed by Pitts and colleagues, these authors and their
-> co-workers have developed a package to support such reasoning in the
-> Isabelle proof tool for Higher Order Logic. This toolkit has been
-> widely used, and although the technology sometimes shows through
-> (e.g. explicit name swapping required in arguments) it is a very good
-> package.
->
-> Up to now, this package has supported single binders such as \lambda.
-> Multiple simultaneous binding (e.g. letrec) had to be coded using
-> iterated single binders. Not only is this coding hard to reason
-> about, it often isn't a correct representation of the intended
-> language. This paper describes a new version of the Isabelle package,
-> "Nominal2", supporting binding of sets and lists of names in the
-> Isabelle/HOL system.
->
-> The amount of work involved is immense, and the first author
-> especially has shown real commitment to continuing development of both
-> theory and working tools. Everything provided in this package is
-> claimed to be a definitional extension of HOL: no assumptions or
-> built-in changes to the logic. For all of these reasons, this is very
-> good work.
+> [...]
>
> However, I recommend improvement of the presentation of the paper
> before it is accepted by LMCS. While the motivation for the work of
@@ -51,7 +27,8 @@
> it would be done in the new system reported in this paper showing why
> the new approach works better in practice.
-Added
+We have expanded on the point why single binders lead to clumsy
+formalisations.
> Although this example is
> one of the main motivations given for the work, there is apparently no
@@ -64,9 +41,8 @@
> advanced tasks in the POPLmark challenge [2], because also there one
> would like to bind multiple variables at once.").
-No time to provide full examples yet. They will be provided
-once Nominal2 becomes more mature and people are using it
-and help to provide theories.
+We proved the main properties about type-schemes in algorithm W.
+Though the complete formalisation 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
@@ -74,50 +50,36 @@
> 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 before the summer 2012.
+release of Isabelle, which should be out in the summer 2012.
At the moment it can be downloaded as a bundle and is ready
-to be used (we have confirmation from two groups for this).
+to be used (there are two groups that already 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
> (2.4) and (2.5).
+We reworded this paragraph.
> Bottom of p.9: The parameters R and fa of the alpha equivalence
> 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.
+
> 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"?
-
+Both are equivalent since sets {x, y} and {y, x} are equal. But we made
+it clearer as you suggest.
> Referee no 2:
>
-> * The paper can be accepted for Logical Methods in Computer Science
-> after minor
-> revisions
->
-> General comments
->
-> This paper describes a new implementation of the nominal_datatype package
-> within the Isabelle/HL theorem prover. This implementation is more modular
-> than previous versions, because it relies on (I think) three non-trivial
-> independent packages, namely the datatype package, the function package, and
-> the quotient package. This implementation is also more powerful than previous
-> versions, because it deals with abstractions that bind multiple names
-> at once,
-> and because it offers two variants of these abstractions (baptised "set" and
-> "set+") where certain structural equivalence laws, namely the exchange of two
-> binders and the elimination/introduction of a vacuous binder, are built
-> directly into the alpha-equivalence relation.
->
-> Overall, I like the paper because it describes a useful piece of software,
-> because the architecture of this software is quite non-trivial and well
-> designed, and because the paper is written in a very understandable style.
-> For these reasons, I believe the paper should be accepted. I do have a series
-> of questions and suggestions for potential improvements and would be happy to
-> review a revised version of the paper if the editor sees fit.
+> [...]
>
> My main criticisms of the paper are:
>
@@ -125,11 +87,19 @@
> The general format at the beginning of section 4 is very clear, but is in
> fact too general: not everything that can be written in this format makes
> sense. The authors then walk the reader through a series of
-> examples of what
+> 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.
+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.
+
> * 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
@@ -148,36 +118,76 @@
> 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
+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.
+
> 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"
+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.
+
> * 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
+
+ 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
+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
+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?
->
+> 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).
+So we have not found a unifying framework yet.
+
> * 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
+> 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. There are object languages,
+> 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
+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.
+
+> 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
@@ -188,7 +198,11 @@
> of structural equivalence anyway. I don't think that the paper provides
> 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.
+
> * 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:
>
@@ -204,24 +218,9 @@
> this example, otherwise set-abstractions will not be very useful in
> practice.
->> datatype trm =
->> Var string
->> | App trm trm
->> | Lam string trm
->> | Let "(string * trm) fset" trm
->> Not a problem. Both finite sets and bags should be possible as
->> constructors within the new package.
->> Best regards and a happy new year!
->> Andrei Popescu
+We can. We added this as an example in the conclusion section.
->
-> Detailed comments
->
-> [Written while I was reading, so sometimes I ask a question whose
-> answer comes
-> a bit later in the paper.]
->
> 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,46 +236,88 @@
> 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
+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.
+
> p.3, "let the user chose" -> "choose"
->
+
+Fixed.
+
> p.5, I am not sure what you mean by "automatic proofs". Do you mean
> automatically-generated proof scripts, or proofs performed automatically by a
> decision procedure, or ... ?
->
+
+Fixed.
+
> p.5, "adaption"
->
+
+Fixed.
+
> p.5, it seems strange to use the symbol "+" for composition, a
> non-commutative
> operation.
->
+
+Yes. This is a "flaw" in the type-class setup. If we want to reuse libraries
+from Isabelle, we have to bite into this "sour" apple.
+
> 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.
+The advantage of our definition is that can be easily stated
+in a theorem prover since it fits into the scheme
+
+ lhs = rhs
+
+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.
+
> Proposition 2.3, item (i) is not very easy to read, because text and math
-> are mixed and "as" happens to be an English word. More importantly, could
+> are mixed and "as" happens to be an English word.
+
+Replaced by bs.
+
+> More importantly, could
> you explain why the hypothesis "finite as" is needed? The proposition seems
> 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
+bs is the set of "even" atoms (a set that is not finite nor co-finite).
+
+ bs supports bs
+
+but
+
+ supp bs = all_atoms !<= bs
+
> p.8, "equivariant functions have empty support". I suppose the converse is
> true, i.e. "functions that have empty support are equivariant". If this is
> correct, please say so.
->
-> p.8, "we used extensively Property 2.1". You mean "Proposition 2.1". Perhaps
-> it would be good to choose distinct numbers for inline equations and for
-> propositions.
->
+
+We have reworded this paragraph.
+
+> p.8, "we used extensively Property 2.1". You mean "Proposition 2.1".
+
+Fixed.
+
> p.8, "we identify four conditions: (i) [...] x and y need to have the same
> set of free atoms". You seem to be saying that fa(x) and fa(y) should be
> equal. But this is too strong; I suppose you mean fa(x) \ as = fa(y) \ bs.
> Please clarify. (Definition 3.1 indeed clarifies this, but I believe that
> the text that precedes it is a bit confusing.)
->
+
+Fixed.
+
> p.9, it seems to me that alpha-equivalence for Set+ bindings (Definition 3.3)
> is in a sense the most general of the three notions presented here. Indeed,
> alpha-equivalence for Set bindings can be defined in terms of it, as follows:
@@ -300,34 +341,73 @@
> more radical
> 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
+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.
+
> 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
+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.
+
> 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. Same remark in a couple of places further
+> an x with infinite support.
+
+Fixed.
+
+> Same remark in a couple of places further
> down on this page. You note that "supp bs = bs" holds "for every finite
> set of atoms bs". Is it *not* the case that this also holds for infinite
-> sets? If so, what *is* the support of an infinite set of atoms? Why not
+> sets? If so, what *is* the support of an infinite set of atoms?
+
+This property only holds for finite sets bs. See above.
+
+> Why not
> adopt a definition of support that validates "supp bs = bs" for *every*
> set of atoms bs? Is there a difficulty due to the fact that what you
> call a "permutation" is in a fact "a permutation with finite support"?
> I think it would be good to motivate your technical choices and clarify
> exactly where/why a finite support assumption is required.
->
+
+This cannot be made as it is very natural to have the property
+that the set of all atoms has empty support. There is no permutation
+that does not fix that set. We cannot see how this can be made
+to work so that
+
+ supp bs = bs
+
+for all sets.
+
> p.11, "The other half is a bit more involved." I would suggest removing
> this rather scary sentence. The proof actually appears very simple and
> elegant to me.
->
+
+Fixed.
+
> p.12, "mutual recursive" -> "mutually recursive"
->
+
+Fixed.
+
> p.12, does the tool support parameterized data type definitions? If so,
> please mention it, otherwise explain whether there is a difficulty (e.g.
> the parameters would need to come with a notion of permutation).
->
+
+Yes. Note added.
+
> p.12, "Interestingly, [...] will make a difference [...]". At this
> point, upon
> first reading, this is not "interesting" but rather frustrating, because it
@@ -336,30 +416,41 @@
> u". Because
> a forward pointer is missing, I cannot find immediately where this is
> explained, and this problem hinders my reading of the beginning of section 5.
->
-> p.13, the type of sets now seems to be "fset" whereas it was "set"
-> previously.
->
+
+We have given a forward pointer.
+
> p.13, the type of atoms now seems to be "name", whereas it was previously
> "atom". The remark on the last line of page 13 leads me to understand that
> "name" refers to one specific sort of atoms, whereas "atom" refers to an
> atom of any sort (right?). The function "atom" converts one to the other;
> but what is its type (is it overloaded?).
->
+
+Yes, atom is overloaded.
+
> p.13, you distinguish shallow binders (binds x in ...) and deep binders
> (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
+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
> much either way.)
->
+
+That would make the definition of fa-function more complicated.
+
> 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? Second, I don't understand why you need this
+> this allowed or excluded?
+
+For practical purposes, this is excluded. But the theory would
+support this case.
+
+> 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
@@ -368,10 +459,11 @@
> (at least, you have not stated that you disallow this). There, occurrences of
> 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? Is this a somewhat ad hoc
-> restriction that simplifies your implementation work, or is there really a
-> deep reason why accepting this clause would not make sense?
->
+> 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.
+
> 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
@@ -413,7 +505,9 @@
> issue. Is it conceivable that an extension of your system could deal with
> telescopes? Other researchers have proposed approaches that can deal with
> them (I am thinking e.g. of ``Binders Unbound'' by Weirich et al.).
->
+
+Yes, we cannot deal with telescopes. We added a comment.
+
> Here is another general question. How would you declare a nominal data type
> for ML patterns? Informally, the syntax of patterns is:
>
@@ -429,17 +523,23 @@
> same sets of names. How would you deal with this? I imagine that one could
> just omit these two side conditions in the definition of the nominal data
> type, and deal with them separately by defining a well-formedness predicate.
+
+Yes, that is how we would exclude non-linear patterns.
+
> One question: in the definition of the "term" data type, at the point where
> one writes "binds bn(p) in t", which variant of the "binds" keyword would one
> use: "binds", "binds(set)", or "binds(set+)"? Does it make any difference,
> considering that a pattern can have multiple occurrences of a name in binding
> position? It would be interesting if you could explain how you would handle
> this example.
->
-> Another interesting (perhaps even more tricky) example is the syntax of the
-> join-calculus. In terms of binding, it is really quite subtle and worth a
-> look.
->
+
+You can write
+
+ binds bn(p) in t,
+ binds(set) bn(p) in t,
+ binds(set+) bn(p) in t
+
+
> p.15, just before section 5, I note that the completion process does *not*
> produce any clause of the form "binds ... in x" (in the Lam case). One could
> have expected it to produce "binds x in x", for instance. One could imagine
@@ -463,23 +563,9 @@
> side of a "binds" clause). As far as I can see, however, you have not
> explicitly forbidden this situation. So, is it forbidden or allowed? Please
> clarify.
->
-> If there is indeed a partition between "terms" and "binders", please justify
-> why things must be so. I can think of a more general and more symmetric
-> approach, where instead of writing "binds bn(p) in t" and considering that "p
-> is a binder" and "t is a term", one would write "binds bn(p) in p t" and
-> consider that p and t play a priori symmetric roles: the only difference
-> between them stems from the fact that we collect the bound names
-> inside p, but
-> not inside t. (I am not suggesting that the user should write this, but that
-> the user syntax could be desugared down to something like this if this makes
-> the theory simpler.) Ah, but I guess that if one were to follow this path,
-> then one would need a way of distinguishing recursive versus non-recursive
-> binders. I guess I see why your design makes sense, but perhaps you should
-> better explain that it is a compromise between several other possible designs
-> (``alphacaml'', ``binders unbound'', etc. are examples of other designs) and
-> how you reached this particular point in the design space.
->
+
+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
@@ -490,12 +576,7 @@
> 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, "we have to add in (5.3) the set [...]". It is not very clear whether
-> you are suggesting that equation 5.3 is incomplete and something should be
-> added to it, or equation 5.3 is fine and you are referring to B' which is
-> there already. I suppose the latter.
->
+
> 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*
@@ -508,45 +589,40 @@
> you are not restricting just *the values* that these functions can
> return, but
> the *syntactic form* of these functions.
->
+
+Fixed.
+
> p.23, "We call these conditions as": not really grammatical.
->
+
+Fixed.
+
> p.23, "cases lemmas": I suppose this means an elimination principle?
->
+
+Yes.
+
> p.23, "Note that for the term constructors" -> "constructor"
->
+
+Fixed.
+
> p.26, "avoid, or being fresh for" -> "avoid, or are fresh for"
->
+
+Fixed.
+
> p.30, "Second, it covers cases of binders depending on other binders,
> which just do no not make sense [...]". I am curious why the designers
> of Ott thought that these cases make sense and you don't. Perhaps this
> point would deserve an example and a deeper discussion?
->
-> p.30, at last, here is the discussion of "binds ... in s t" versus
-> "binds ... in s, binds ... in t". I see that the difference in the
-> two interpretations boils down to an abstraction whose body is a pair,
-> versus a pair of abstractions. It is indeed interesting to note that
-> these notions coincide for single-name abstractions, and for list
-> abstractions, but not for set and set+ abstractions.
->
+
+We have added more comments why such binders would not make sense
+for alpha-equated terms (fa-functions would not lift). We do not
+know why Ott allows them - probably because they do not establish
+a reasoning infrastructure for alpha-equated terms.
+
> p.32, "It remains to be seen whether properties like [...] allow us
> to support more interesting binding functions." Could you clarify
> what you mean? Do you mean (perhaps) that fa_bn(x) could be defined
> as fa_ty(x) \ bn(x), regardless of the definition of bn(x), instead
> of by induction over x? Do you mean something else?
->
-> The example in Figures 1 and 2 do not seem very interesting to me. It
-> involves single binders and flat lists of binders. Not much subtlety going on
-> here. I think this example could be reduced in size without losing
-> anything in
-> terms of content. And perhaps a trickier example could be added (I have two
-> suggestions, which I mentioned above already: ML with conjunction and
-> disjunction patterns; and the join-calculus).
->
->
->
->
->
->
->
+Yes.
+