--- 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.
-