--- a/LMCS-Paper/Paper.thy Wed Feb 29 04:56:06 2012 +0000
+++ b/LMCS-Paper/Paper.thy Wed Feb 29 16:23:11 2012 +0000
@@ -115,7 +115,8 @@
type-variables. While it is possible to implement this kind of more general
binders by iterating single binders, like @{text "\<forall>x\<^isub>1.\<forall>x\<^isub>2...\<forall>x\<^isub>n.T"}, this leads to a rather clumsy
formalisation of W. For example, the usual definition when a
- type is an instance of a type-scheme requires the following auxiliary \emph{unbinding relation}
+ type is an instance of a type-scheme requires in the iterated version
+ the following auxiliary \emph{unbinding relation}
\[
\infer{@{text T} \hookrightarrow ([], @{text T})}{}\qquad
@@ -124,11 +125,12 @@
\]\smallskip
\noindent
- which relates a type-scheme with a list of variables and a type. The point of this
- definition is to get access to the bound variables and the type-part of a type-scheme
- @{text S}, though in general
- we will only get access to some variables and some type @{text T} that are
- ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation, not a function.
+ which relates a type-scheme with a list of type-variables and a type. The point of this
+ definition is: given a type-scheme @{text S}, how to get access to the bound type-variables
+ and the type-part of this type-scheme? The unbinding relation gives an answer, though in general
+ we will only get access to some type-variables and some type that are
+ ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
+ for alpha-equated type-schemes.
Still, with this
definition in place we can formally define when a type is an instance of a type-scheme as
@@ -137,19 +139,20 @@
\]\smallskip
\noindent
- meaning there exists a list of variables @{text xs} and a type @{text T'} to which
+ meaning there exists a list of type-variables @{text xs} and a type @{text T'} to which
the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
@{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
The problem with this definition is that we cannot follow the usual proofs
that are by induction on the type-part of the type-scheme (since it is under
- an existential quantifier). The representation of type-schemes using iterations of single binders
- prevents us from directly ``unbinding'' the bound variables and the type-part of
- a type-scheme. The purpose of this paper is to introduce general binders, which
+ an existential quantifier and only an alpha-variant). The representation of
+ type-schemes using iterations of single binders
+ prevents us from directly ``unbinding'' the bound thye-variables and the type-part.
+ The purpose of this paper is to introduce general binders, which
allow us to represent type-schemes so that they can bind multiple variables at once
and as a result solve this problem.
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
+ mechanisms for binding single variables have so far not fared very well with
the more advanced tasks in the POPLmark challenge \cite{challenge05},
because also there one would like to bind multiple variables at once.
@@ -500,7 +503,7 @@
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
two-place permutation operation written
- @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+ @{text "_ \<bullet> _ "} and having the type @{text "perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
where the generic type @{text "\<beta>"} is the type of the object
over which the permutation
acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
@@ -623,7 +626,7 @@
\end{equation}\smallskip
\noindent
- If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, this definition is equivalent to
+ If a function is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, say, this definition is equivalent to
the fact that a permutation applied to the application
@{text "f x"} can be moved to the argument @{text x}. That means for
such functions, we have for all permutations @{text "\<pi>"}:
@@ -898,16 +901,14 @@
\end{equation}\smallskip
\noindent
- and also
+ and also set
\begin{equation}\label{absperm}
- @{thm permute_Abs(1)[where p="\<pi>", no_vars]}
+ @{thm permute_Abs(1)[where p="\<pi>", no_vars, THEN eq_reflection]}
\end{equation}\smallskip
\noindent
- The second fact derives from the definition of permutations acting on pairs
- \eqref{permute} and alpha-equivalence being equivariant
- (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show
+ With this at our disposal, we can show
the following lemma about swapping two atoms in an abstraction.
\begin{lem}
@@ -963,7 +964,8 @@
\noindent
This is because for every finite set of atoms, say @{text "bs"}, we have
- @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+ @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.\footnote{Note that this is not
+ the case for infinite sets.}
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes
the first equation of Theorem~\ref{suppabs}. The others are similar.
@@ -1043,7 +1045,7 @@
recursive arguments need to satisfy a `positivity' restriction, which
ensures that the type has a set-theoretic semantics (see
\cite{Berghofer99}). If the types are polymorphic, we require the
- type variables stand for types that are finitely supported and over which
+ type variables to stand for types that are finitely supported and over which
a permutation operation is defined.
The labels @{text "label"}$_{1..l}$ annotated on the types are optional. Their
purpose is to be used in the (possibly empty) list of \emph{binding
@@ -1200,7 +1202,8 @@
\begin{equation}\label{letrecs}
\mbox{%
\begin{tabular}{@ {}l@ {}l}
- \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
+ \isacommand{nominal\_datatype}~@{text "trm ="}\\
+ \hspace{5mm}\phantom{$\mid$}~\ldots\\
\hspace{5mm}$\mid$~@{text "Let as::assn t::trm"}
& \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
\hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
@@ -1236,11 +1239,14 @@
\noindent
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
- out different atoms to become bound, respectively be free, in @{text "p"}.
- (Since the Ott-tool does not derive a reasoning infrastructure for
- alpha-equated terms with deep binders, it can permit such specifications.)
- For convenience we exlude such specifications even if @{text "bn\<^isub>1"} and
- @{text "bn\<^isub>2"} are the same binding functions, which would otherwise be harmless.
+ out different atoms to become bound, respectively be free,
+ in @{text "p"}.\footnote{Although harmless, in our implementation
+ we exlude such specifications even
+ if @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} are the same binding
+ functions.}$^,$\footnote{Since the Ott-tool does not derive a reasoning
+ infrastructure for
+ alpha-equated terms with deep binders, it can permit such specifications.}
+
We also need to restrict the form of the binding functions in order to
ensure the @{text "bn"}-functions can be defined for alpha-equated
@@ -2228,7 +2234,7 @@
is straightforward to establish that the sizes decrease in every
induction step. What is left to show is that we covered all cases.
To do so, we have to derive stronger cases lemmas, which look in our
- running example are as follows:
+ running example as follows:
\[\mbox{
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
--- 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*