diff -r fb201e383f1b -r da575186d492 LMCS-Review --- a/LMCS-Review Tue Feb 19 05:38:46 2013 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,619 +0,0 @@ - -> 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. -> -> [...] -> -> 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. - -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 -> 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."). - -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 -> 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 Autumn 2012. -At the moment it can be downloaded as a bundle and is ready -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 -> (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 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"? - -Both are equivalent since sets {x, y} and {y, x} are equal. But we made -it clearer as you suggest. - -> Referee no 2: -> -> [...] -> -> 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. - -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. 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 -> 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. - -We are not sure whether we can make progress with this. There is such a -"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" (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 -> 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. 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 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 -> 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 (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 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, -> 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 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 -> 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, -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; 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 -> 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.) - -From our experience, once a feature is included, applications will -be found. Case in point, the set+ binder arises naturally in the -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 -> -> 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. - -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 -> 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. - -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 -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" - -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 finitely supported x. -The advantage of our definition is that can be easily stated -in a theorem prover since it fits into the scheme - - 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. - -> 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. - -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. - -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: -> -> (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? - -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+. 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" - -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, 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 -> 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? - -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 -> 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. - -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. - -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 -> 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? - -For practical purposes, this is excluded. But the theory would -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 -> 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? - -The problem is that bn1 and bn2 can pick out different atoms to -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, -> 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.). - -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: -> -> 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. - -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. - -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 -> 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. - -It is disallowed. We clarified the text. - -> 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. - -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? - -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? - -Yes. -