nominal2: comparison LMCS-Review

equal deleted inserted replaced

-:860df8e1262f
+:d3d5225f4f24
 > 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,
 > 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.
-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
 > 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.").
-No time to provide full examples yet. They will be provided
+We proved the main properties about type-schemes in algorithm W.
-once Nominal2 becomes more mature and people are using it
+Though the complete formalisation is not yet in place.
-and help to provide theories.
 > 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 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:
 >
 > * 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
+>   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
 >   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:
 >   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\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
+>   all, very few properties seem to be required of the basic abstraction forms,
->   few properties seem to be required of the basic abstraction forms,
+>   so why not let the user define new ones?
-> 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
+>   that dealing with structural equivalence should be left to the user, because
-> 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
 >   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.
 > * 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
 >
 >   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.
->> datatype trm =
+We can. We added this as an example in the conclusion section.
->>       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
->
-> 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
 > 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
+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
+We have reworded this paragraph.
-> it would be good to choose distinct numbers for inline equations and for
-> propositions.
+> 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)
 > 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+. 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
 > 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"
+We have given a forward pointer.
-> 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?).
->
+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
 > 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
+> in t2", which seems to be of a similar nature?
-> restriction that simplifies your implementation work, or is there really a
-> deep reason why accepting this clause would not make sense?
+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
 > telescope,
 > and in addition all of the names introduced by the telescope are considered
 > 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)
 > 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.
->
-> Another interesting (perhaps even more tricky) example is the syntax of the
+You can write
-> join-calculus. In terms of binding, it is really quite subtle and worth a
-> look.
+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
 > (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
+It is disallowed. We clarified the text.
-> 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
 > 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?
->
-> p.30, at last, here is the discussion of "binds ... in s t" versus
+We have added more comments why such binders would not make sense
-> "binds ... in s, binds ... in t". I see that the difference in the
+for alpha-equated terms (fa-functions would not lift). We do not
-> two interpretations boils down to an abstraction whose body is a pair,
+know why Ott allows them - probably because they do not establish
-> versus a pair of abstractions. It is indeed interesting to note that
+a reasoning infrastructure for alpha-equated terms.
-> 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
+Yes.
-> 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).
->
->
->
->
->
->
->

changeset 3126	d3d5225f4f24
parent 3104	f7c4b8e6918b
child 3129	8be3155c014f