--- a/LMCS-Review Wed Feb 29 04:56:06 2012 +0000
+++ b/LMCS-Review Wed Feb 29 16:23:11 2012 +0000
@@ -27,8 +27,8 @@
> 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 why single binders lead to clumsy
-formalisations.
+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
@@ -41,8 +41,9 @@
> 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.
-Though the complete formalisation is not yet in place.
+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
@@ -50,9 +51,9 @@
> 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 the summer 2012.
+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 already use Nominal2 and
+to be used (there are two groups that use Nominal2 and
only occasionally ask questions on the mailing list).
> A few more specific points:
@@ -68,7 +69,7 @@
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.
+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 [...]"
@@ -92,13 +93,16 @@
> 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.
+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.
+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
@@ -120,11 +124,11 @@
> 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
+"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". This led
-us to isolate the notions of shallow, deep and recursive binders.
+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
@@ -132,11 +136,11 @@
> 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"
+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 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.
+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
@@ -146,7 +150,7 @@
> "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
+literature (pointers in the paper). Assume all_atoms is the set of all atoms then
supp all_atoms = {}
@@ -157,9 +161,9 @@
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
+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,
@@ -168,8 +172,8 @@
> 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.
+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
@@ -180,12 +184,12 @@
> 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 an application
+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. 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.
+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
@@ -201,7 +205,7 @@
From our experience, once a feature is included, applications will
be found. Case in point, the set+ binder arises naturally in the
-psi-calculus.
+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:
@@ -220,7 +224,6 @@
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,
@@ -237,11 +240,11 @@
> 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
+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.
+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"
@@ -269,11 +272,11 @@
> 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.
+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
- lhs = rhs
+ constant args = term
Your definition as the least set...does not fit into this simple
scheme. Our definition has been described extensively elsewhere,
@@ -291,7 +294,7 @@
> 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
+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
@@ -344,10 +347,12 @@
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.
+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"
@@ -356,12 +361,9 @@
> 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.
+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
@@ -433,7 +435,7 @@
> 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
+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
@@ -448,7 +450,7 @@
> this allowed or excluded?
For practical purposes, this is excluded. But the theory would
-support this case.
+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
@@ -462,7 +464,7 @@
> in t2", which seems to be of a similar nature?
The problem is that bn1 and bn2 can pick out different atoms to
-be free and bound in p. This requires to exclude this case.
+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
@@ -566,17 +568,6 @@
It is disallowed. We clarified the text.
-> OK, now I see that, since you allow ``recursive binders'', there is not a
-> partition between ``terms'' and ``binders''. A recursive binder appears both
-> on the left- and right-hand sides of a binds clause. Do you require that it
-> 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, "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*