--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/LMCS-Review Thu Dec 29 12:40:36 2011 +0000
@@ -0,0 +1,525 @@
+
+> Referee no 1:
+>
+> * The paper can be accepted for Logical Methods in Computer Science
+> after minor
+> revisions
+>
+> NUMBER : LMCS-2011-675
+> TITLE : General Bindings and Alpha-Equivalence in Nominal Isabelle
+> AUTHOR(S) : Christian Urban, Cezary Kaliszyk
+>
+> Recommendation: The paper can be accepted for Logical Methods in
+> Computer Science after minor revisions.
+>
+> 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
+> this paper is clear to anyone who has tried to formalize such
+> reasoning, it is not explained in the paper. E.g. on p.1 "However,
+> Nominal Isabelle has fared less well in a formalisation of the
+> 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. 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
+> provided. Similarly for the second motivating example (on p.2 "The
+> need of iterating single binders is also one reason why Nominal
+> 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.").
+>
+> 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.
+>
+> A few more specific points:
+>
+> Bottom of p.7: I don't understand the paragraph containing equations
+> (2.4) and (2.5).
+>
+> 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.
+> 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"?
+>
+>
+> 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:
+>
+> * The definition of the "nominal signature" language is not completely clear.
+> 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
+> 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.
+>
+> * 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
+> for the authors, but I would like them to go further in this direction:
+> identify more elementary building blocks ("combinators", if you will),
+> study their properties in isolation, and in the end combine them to
+> obtain a very simple explanation of the "nominal signature" format
+> that is exposed to the user. In the present state of the paper, the
+> design of the "nominal signature" format seems somewhat ad hoc: the
+> format of the "binds" clauses is subject to several restrictions;
+> there seems to be a distinction between "binders" and ordinary
+> "terms"; there is a distinction between "recursive" and "non-recursive"
+> binders, and a distinction between "shallow" and "deep" binders. If
+> one could identify a small number of elementary building blocks and
+> explain/motivate the design of the surface specification language in
+> terms of these elementary notions, the paper might become all the more
+> compelling.
+>
+> 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.
+>
+> * 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.
+>
+> * 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?
+>
+> * 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. 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
+> conjunction.) Thus, one may fear that in many cases, the set and set+
+> abstractions will not be sufficiently powerful to encode the desired
+> structural equivalence, and the user will need to explicitly define
+> a notion
+> 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.)
+>
+> * 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
+>
+> where the xi's are bound in t (this is a non-recursive multiple-let form)
+> and the order of the definitions does not matter (that is, "let x1 = t1
+> and x2 = t2 in t" is alpha-equivalent to "let x2 = t2 and x1 = t1 in t")?
+> Can you use a set-abstraction to achieve this? I am guessing that this
+> might be possible, if one represents the definitions "x1 = t1 and ..."
+> using a set of pairs (or a map of names to terms) as opposed to a list
+> 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.
+>
+> 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,
+> I am not
+> sure that the ML type system (or its inference algorithm) is a good
+> illustration. If one examines the typing rules of Core ML, one finds that
+> their premises involve a notion of equality between *types* (for
+> instance, the
+> function application rule requires that the types of the formal and actual
+> arguments match) but do not involve any notion of equality between *type
+> schemes*. Type schemes are constructed and eliminated; they are never
+> 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.
+>
+> p.3, "let the user chose" -> "choose"
+>
+> 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 ... ?
+>
+> p.5, "adaption"
+>
+> p.5, it seems strange to use the symbol "+" for composition, a
+> non-commutative
+> operation.
+>
+> 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?
+>
+> 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
+> 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).
+>
+> 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.
+>
+> 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.)
+>
+> 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:
+>
+> (as, x) =_{Set} (bs, y)
+> if and only if
+> (as, (as, x)) =_{Set+} (bs, (bs, y))
+>
+> That is, I am comparing abstractions whose body has type "atom set * beta".
+> The comparison of the set components forces condition (iv) of Definition 3.1.
+> Similarly, alpha-equivalence for List bindings can be defined in terms of it,
+> as follows:
+>
+> (as, x) =_{List} (bs, y)
+> if and only if
+> (set as, (as, x)) =_{Set+} (set bs, (bs, y))
+>
+> That is, I am comparing abstractions whose body has type "atom list * beta".
+> Am I correct to think that one can do this? If so, could this help eliminate
+> some redundancy in the paper or in the implementation? And, for a
+> 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?
+>
+> p.10, "in these relation"
+>
+> p.10, isn't equation (3.3) a *definition* of the action of permutations
+> on the newly defined quotient type "beta abs_{set}"?
+>
+> 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
+> 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
+> 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.
+>
+> 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.
+>
+> p.12, "mutual recursive" -> "mutually recursive"
+>
+> 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).
+>
+> p.12, "Interestingly, [...] will make a difference [...]". At this
+> point, upon
+> first reading, this is not "interesting" but rather frustrating, because it
+> does not sound natural: my understanding would be very much simplified if
+> "binds ... in t u" was equivalent to "binds ... in t, binds ... in
+> 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.
+>
+> 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?).
+>
+> 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.
+>
+> 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.)
+>
+> 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
+> 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
+> the case of single binders, you seem to allow "binds x y in t1, binds
+> y in t2"
+> (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?
+>
+> 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,
+> and in addition all of the names introduced by the telescope are considered
+> bound by the telescope in some separate term. I am thinking of
+> something along
+> the following lines:
+>
+> nominal_datatype trm =
+> | Var name
+> | Let tele::telescope body::trm binds bn(tele) in body
+> | ...
+>
+> and telescope =
+> | TNil
+> | TCons x::name rhs::trm rest::telescope binds x in rest
+>
+> binder bn::telescope => atom list
+> where bn (TNil) = []
+> | bn (TCons x rhs rest) = [ atom x ] @ bn(rest)
+>
+> You write that "if we would permit bn to return y, then it would not be
+> respectful and therefore cannot be lifted to alpha-equated lambda-terms". I
+> can see why there is a problem: if "x" is considered bound (therefore
+> anonymous) in the telescope "TCons x rhs rest", then it cannot possibly be
+> returned by a (well-behaved) function "bn". I think that the answer to this
+> problem should be: we must pick an appropriate notion of alpha-equivalence
+> for telescopes, and this notion of alpha-equivalence must *not* consider x
+> as anonymous in "TCons x rhs rest". Instead, x must be considered free in
+> this telescope. The telescopes "TCons x rhs TNil" and "TCons y rhs TNil"
+> must be considered distinct. Of course we could achieve this effect just by
+> removing the clause "binds x in rest", but this would lead to a notion of
+> alpha-equivalence for "Let" terms which is not the desired one: when writing
+> "let (x1 = t1; x2 = t2) in t", we would like x1 to be bound in t2, and this
+> will not be the case if we omit "binds x in rest" in the above definition.
+> I conclude that your design (which seems very reasonable) cannot currently
+> express telescopes. It would be nice if you could explicitly discuss this
+> 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.).
+>
+> Here is another general question. How would you declare a nominal data type
+> for ML patterns? Informally, the syntax of patterns is:
+>
+> p ::=
+> x (variable)
+> | (p, p) where bn(p1) and bn(p2) are disjoint (pair)
+> | (p | p) where bn(p1) = bn(p2) (disjunction)
+> | ...
+>
+> In the case of a pair (or conjunction) pattern, one usually requires that the
+> two components bind disjoint sets of names, whereas in the case of a
+> disjunction pattern, one requires that the two components bind exactly the
+> 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.
+> 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.
+>
+> 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
+> that, for *every* constructor argument t, there is a clause of the
+> form "binds
+> .. in t". Here, you adopt a different approach: you seem to be partitioning
+> the constructor arguments in two categories, the "terms" (which after
+> completion appear in the right-hand side of exactly one "binds" clause) and
+> the "binders" (which appear in the left-hand side of at least one "binds"
+> clause). Please clarify whether this is indeed the case. (You have
+> presented a
+> series of data type definitions that you forbid, but in the end, you should
+> present a succinct summary of what is allowed.) Also, I seem to understand
+> that the following definition is forbidden:
+>
+> nominal_datatype trm =
+> | Foo t1::trm t2::trm binds bn(t1) in t2, binds bn(t2) in t1
+>
+> (for some definition of "bn"). This would be forbidden because t1 and t2 are
+> used both as "terms" and as "binders" (both on the left-hand and right-hand
+> 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.
+>
+> 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, "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*
+> 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
+> "my_empty_set" is a user-defined function that always returns the empty set;
+> otherwise the third bullet would apply and we would end up considering "z_i"
+> as neither free nor bound. You have mentioned near the top of page 15 that
+> binding functions "can only return" certain results. You should clarify that
+> you are not restricting just *the values* that these functions can
+> return, but
+> the *syntactic form* of these functions.
+>
+> p.23, "We call these conditions as": not really grammatical.
+>
+> p.23, "cases lemmas": I suppose this means an elimination principle?
+>
+> p.23, "Note that for the term constructors" -> "constructor"
+>
+> p.26, "avoid, or being fresh for" -> "avoid, or are fresh for"
+>
+> 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.
+>
+> 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).
+>
+>
+>
+>
+>
+>
+>
+