Date: Wed, 23 May 2007 14:56:35 +0100
Message-Id: <200705231356.l4NDu6IH002530@rpc74.cs.man.ac.uk>
From: csl07@easychair.org
To: dale@lix.polytechnique.fr
Subject: CSL'07: reviews on your paper
Dear authors,
Please find below the reviews on your paper.
Thank you for submitting to CSL.
All the best,
Jacques Duparc
---------------------------------------------
Paper: 6
Title: Least and greatest fixed points in linear logic
-------------------- review 1 --------------------
The authors extend first-order multiplicative and additive fragment of linear logic MALL by least and greatest fixed points and study proof-theoretical principles for this logic.
They establish a cut-elimination theorem and present a focused proof system
that is compete for the logic. The show how this proof theory can be applied to intuitionistic logic with induction and co-induction.
The approach of this paper is interesting and the results seem relevant
for linear logic, although this is hard to judge for an outsider.
My criticism on this paper concerns its presentation. It is written for
insiders in the field of linear logic, not at all taking into account that CSL is a broad conference in logic in computer science. Surely, the majority of
the audience is not familiar with MALL and with much of the jargon related to linear logic.
I strongly suggest to the authors to provide more background and to make a real
effort to render the paper more accessible for a broad readership.
-------------------- review 2 --------------------
The article introduces an extension of multiplicative additive linear
logic with equality by least and greatest fixed points. A calculus is
presented that enjoys (semantic) cut-elimination. Also a "focused"
variant of the proof system is presented and shown to be complete with
respect to the original calculus. Even though this "focused" variant
resembles other focused calculi, no formal statement about the special
properties of these focused proofs are given. Finally, a fragment of
intuitionistic logic with fixed points is embedded into the proposed
system. This fragment is defined not only by the language, but also by
the way the proofs look like. Therefore this fragment is hard to grasp
and the significance of this property remains vague.
Cut-elimination is inherited from that of second order linear logic by
a back and forth translation. A proof of cut-elimination in this way
does not provide either bounds on the size of the normal proofs nor an
operational semantics on proofs.
My main criticism about this article is, that linearity is a
restriction and when extending it to stronger systems one should make
sure that one still has at least some benefits from confining oneself
to such a typing discipline. However, I fail to find any statement in
that direction in the article. There is no statement about the
complexity of cut-elimination or the complexity of proof search or any
desirable properties of its models. In fact, no semantics is provided,
so that we not even can ask whether the calculus is sound or complete
in any reasonable sense.
Even worse, the explanation about complete sets of unifiers and the
inequality rule suggest that the authors seems to consider infinite
proofs as well. As there is no formal definition of what a proof is,
the reader has to guess whether these infinite objects have to be
presented effectively, whether transformations are claimed to be
effective, whether stronger notions of uniformity are to be
considered, and so on. In either case all desirable properties of
linear logic, like efficient cut-elimination, interesting models, or
similar become even more vague by this device.
Similarly, the benefit of considering the "focused proof system"
remains unclear. What do we gain (for example for proof search) by
considering the focused rather than the original proof system? No
statement in this direction is provided. Also, since completeness is
only shown with respect to the first system and not with respect to
some notion of model, what is the significance of this?
The proofs provided in the article or the associated technical report
[BM07] are pretty sketchy and hard, or in some cases even impossible,
to follow. I therefore wasn't able to check the correctness of all the
theorems, propositions and lemmata; however the claimed statements
seem plausible.
Also in other points the presentation lacks the usual standards
expected for a scientific conference. In a sequence of iterated
rereading the whole article, the reading has to try and find out, what
the precise nature of objects under consideration is, how explanations
or theorems are to be understood. What definitely remains unclear is
the status of negation. On the one hand you assume it to be part of
the meta language, on the other hand, Definition 1 of \bar B requires
an explicit negation constructor. Unless you allow negated variables,
the negation symbol cannot be understood at the meta level. In any
case, negation constructors or negated variables would both destroy
the monotonicity property, used in various proofs.
So in the present form it is not possible to judge what the merits of
this article are, if any. I therefore strongly encourage the authors
to very carefully revise their article. In its present form it doesn't
seem ready for publication.
Typos and Comments to individual parts of the text
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
abstract, l6 "cut-elimination elimination theorem". remove second
occurrence of "elimination"
p2, paragraph -3 (starting with "Besides considering..."). I strongly
disagree with the argument here. Firstly, you see it as an advantage
that fixed points come as de-Morgan duals; but so do the exponentials
and all the other connectives. Hence, I fail to see why adding(!)
fixed points should give more symmetry than we had without. Secondly,
if it "will be rather easy to develop a focusing proof system [...]",
then just do it! This might be a more interesting result than the
calculus presented here.
p3, paragraph before first displayed formula, and other places. I know
that it is a consequence of the LNCS style, but having boldface
letters for \vec t is hard to distinguish from normal t in math
mode. Using the option "orivec" or choosing some other notation might
help.
p3, paragraph before Definition 1. You state that there are "no atoms"
in your grammar. But what then are the "s=t" formulae?
p3, same paragraph. You have stated that s,t range over
terms. Here you use it as types. A different letter would be more
consistent and facilitate reading.
p4, l4 "only syntactical". Note that a syntactic condition is
*stronger* than a corresponding semantic condition. It does not only
state a property to hold, but also that it is presented in a very
particular way.
p4, after Proposition 1. Stating a PhD thesis of 2004 as reference for
something considered "standard" is not very convincing. Even though
the thesis is available online and definitely a sound reference, I
doubt that every reader is familiar with every PhD thesis and if the
result really is standard, some better reference should be available.
p5, Example 2. Note that a statement \mu(\lambda p.p) o-o 0 does *not*
imply unprovability of \mu(\lambda p.p) unless you have already shown
consistency. However, I lack such a proof.
p5, Example 3. The notion of "infinite unfolding" is not clear. It
sounds like a semantic notion, but you haven't defined any
semantics. If is a syntactical notion, "unfolding" in which
sense. Aren't your proofs well-founded?
p8, proof of Theorem 2. The definition of \mu(\Pi) is as "height of
\Pi" is not clear, unless one looks it up in [BM07]. However, if I
have to read the technical report anyway to understand your proof
sketch, I don't need the proof sketch any more.
-------------------- review 3 --------------------
1) The authors extend the first-order theory of MALL (multiplicative - addi
tive linear logic) with two operators, least and greatest fixed points. The
se two operators provide a new way of dealing with unbounded behavior which
is alternative to the exponential connectives used in LL (full linear logi
c).
2) They provide a sequent calculus for their MALL logic with fixed points,
and prove a cut-elimination theorem for it.
3) Moreover, they provide a sound and complete focused proof system for it,
in the spirit of Andreoli.
4) They also embed classical intuitionistic first-order logic, augmented wi
th least and greatest fixed points, into their MALL logic with fixed points
.
The paper is quite well written, with useful and illustrative examples (p.
10) that emphasize the expressivity of these two new operators. The results
and the proofs, even though not detailled, seem correct to me. Points 1) t
o 3) above seem very interesting to me, and for that reason I recommend tha
t the paper be accepted. Yet, point 4) above seems rather anecdotal, since
first-order classical intuitionistic logic already enjoys nice proof system
s. Moreover, A crucial gap in the paper is the lack of comparison between t
he expressivity of fixed point operators and that of the exponential: is MA
LL with fixed points more or less expressive than LL, or are the two uncomp
arable?
More detailled comments follow:
p.1, abstract, line 6-7: cut elimination elimination -> cut elimination
p.3, line 12: formulas are denoted by P, Q, R: P, Q and R appear nowhere la
ter on in the definition!
p.3: the authors choose simply typed lambda-calculus as the language of ter
ms for their logic. Then, formuals are defined syntactically over terms, an
d a simply typed lambda-calculus over formulas and terms is used. This lead
s to great confusion since one has two different levels of lambda calculus,
one for terms, and one over terms and formulas, which are notationally und
istinguishable. It is for instance hard to understand from Definition 1 tha
t a body is actually not a term!
Morevoer, the assumption that terms are actually lambda terms is never use
d. I recommend therefore that the laguage of terms remains unprecised.
Defnition 1 is also rather unclear: the involutive negation is applied indu
ctively in the definition on lambda terms, without any explanation of what
it might mean. A careful reader may notice that these lambda terms have act
ually type o, and are formulas, but it would not harm to precise a bit more
:
-emphasize that type o is used only for formulas
-for the fixed point operators, precise the type of B
-in Definition 1, give a type decoration for p and for x, and emphasize the
fact that the negation applies only on objects of type o.
-how does Definition 1 apply when n=0?
p.3, line -4 form -> forms, does -> do
p.4, Proposition 1: what is a co-invariant? the reader has to wait until re
ading p.9, line 13 for an explanation, the right place for doing it is at t
he first occurence of the term.
p.4, Definition 2: do the terms asynchronous and synchronous come from Andr
eoli? If so, give a reference here.
p.8, line 6-7: mu(pi): the letter mu has already another use, please chose
another letter.
p.9, line 21: what other observations?
p.12, line 10: it -> its
-------------------- review 4 --------------------
In this paper the extension of linear logic with fix points is defined.
The logic is shown to have cut elimination
and the focused proof system for this logic is constructed. The
resulting logic is powerful and elegant. The
results are new and accurate, The most interesting result is focusing
proof for fix point operators. The paper is
very well written.