From: csl07@easychair.org
Date: 23 mai 2007 16:05
Subject: CSL'07: reviews on your paper
To: alexis.saurin@normalesup.org
Dear authors,
Please find below
a)instructions on submission of the final version,
b)reviews on your paper.
All the best,
Jacques Duparc
----------------------------------------------------------------------
INSTRUCTIONS FOR AUTHORS
The deadline for submission is 23:59 GMT 18th june 2007.
The final version is restricted to 15 pages.
Please follow the instructions below to prepare and submit your document.
1. Read carefully and follow precisely the instructions for authors at
http://www.springer.de/comp/lncs/authors.html
2. Prepare your manuscript using LaTeX, preferably LaTeX2e, with the
corresponding llncs class you may find at the preceding link.
Note that you do not have to number the pages of your document because
the llncs stle automatically arranges this.
Please do not change the page layout and font size!
3. Download a copyright form at
http://www2.unil.ch/csl07/pictures/copyright.pdf .
You need to fill it up and sign it (one author may sign on behalf of
all the authors of the paper). Then,
- (preferably) e-mail a scanned version of it to: orgcsl07@unil.ch
- or fax it to: + 41 21 692 35 85
- or snail mail it to:
Mme Elisabeth Fournier Pulfer
Quartier UNIL-Dorigny
Internef
CH-1015 Lausanne
(Switzerland)
4. Submit to orgcsl07@unil.ch a ZIP-compressed archive with the
following source files:
(i) a single .tex file for the entire paper
containing all macros and bibliographical references
(ii) ps/eps or pdf/jpg files for all figures
(iii) auxiliary files and fonts you have used with
your source files
(Iv) final pdf file
(v) a readme giving the first and last names of
all the authors of the paper, as well as the name and the
e-mail adress of the corresponding author
Please name the compressed archive csl07-XXX.zip, where XXX is your
paper number. Likewise, name the single file with your text
csl07-XXX.tex and the pdf file for the entire paper csl07-XXX.pdf
Email the entire archive to orgcsl07@unil.ch
If you have any question, or trouble with the final submission, please
contact orgcsl07@unil.ch
---------------------------------------------
Paper: 100
Title: From proofs to focused proofs: a modular proof of focalization
in Linear Logic.
-------------------- review 1 --------------------
This is a well-written paper on focused proofs in linear logic. It
gives a new proof of the completeness of
focused proofs in terms of proof transformation. The modular structure
of the proof permits extensions
to larger systems.
A key component of the proof is the construction of a focalization
graph showing how focalization
is organized within a cut-free proof.
I think that this paper make a significant contribution to linear
logic, and should be accepted for CSL.
-------------------- review 2 --------------------
Summary: This paper gives a new proof of the focussing property for proofs
of classical linear logic, originally proved by Andreoli, which restricts
proofs to a form enabling much more efficient proof search. The basis for
the focussing process is the focalization graph which can be constructed
from an arbitrary cut free LL proof, and from which a focalized proof can be
read off.
Significance: Focussing is one of *the* key aspects of linear logic proofs
--- very appropriate for CSL as it is a proof theoretic property, but
important both for semantics and for proof search and thus logic
programming etc. Since the paper is concerned with a new proof of an
existing result, we can ask what it adds to the original. As is better
understood now, perhaps, than 15 years ago, (and argued here), focussing is
a process, rather than simply a property of proofs, and this paper
contributes to this perspective by analyzing it as such, rather than a
series of rather disjointed properties. It's not completely clear that
Andreoli's method's don't extend (relatively straightforwardly) to variant
logics, although one could say that the notion of focalization graph does
give a clear basis and criterion for success (acyclicity) for any such
extension. But a better demonstration of this point would be to actually use
it to prove new results.
Originality: The paper is original inasmuch as it differs from and improves
on Andreoli's proof, which has also been developed by others. There clearly
are elements of Andreoli's approach here (particularly to the exponentials):
a deeper analysis would be required to determine the relation between the
two proofs. But in any case, the way of organising the proof using the novel
notion of focalization graph is an original contribution.
Exposition and Presentation: In some respects, this is a well written paper:
the explanation of the issues at most points is good. In other ways it lacks
cohesion, though. For example, the \Sigma_3 system is introduced, but not
really related to the focalization process, which is described informally.
I don't feel that there's enough detail given on e.g. multi-focalization to
justify its inclusion at the expense of (e.g.) the example in the appendix.
The presentation is poor in that the paper leaves the impression of having
been written in a rush and possibly not read before it was submitted ---
there are very many typos. (Too many for me to want to list them.)
Conclusion:
This is an interesting result, and worth accepting for CSL. However, if it
is accepted, the authors should revise it (at least proofread and spellcheck
it properly).
-------------------- review 3 --------------------
This paper provides a new proof of the Focussing property of Linear
Logic. Compared to the original proof in Andreoli 1993, the authors
claim the new proof is simpler and more modular. Furthermore, it is
more general, in the sense that it shows that the polarity assignment
for atomic formulas, which is essential to Focussing, need not be
decided globally (on the basis of the atoms), but can be decided
locally at each step of the proof where it is needed (occurrence based
decision).
The new proof of the Focussing property is elegant and captures in a
much crisper way than the original proof the gist of the argument. The
notion of "focalization graph" is the key to this approach. I believe
its presentation could be slightly simplified to make it more readable
(see suggestion at the end of this review).
The first sentence of Section 3.3 is essentially true, and essential
for the sequel, but it is insufficiently justified. Strictly speaking,
the fact that an active formula $F$ is not pointed to by any other
active formula in the focalization graph is equivalent to "any border
sequent containing a positive subformula of $F$ has no negative
subformula of any active formula". Instead, the first sentence of
Section 3.3 reads "no border sequent contains a positive subformula of
$F$". There is a missing step here, namely that any border sequent
must contain a negative subformula of an active formula. This is a
consequence of both the maximality of the positive trunk and the fact
that the conclusion is a positive sequent. And by the way, that is
correct only if Definition 3 of the positive trunk is altered so that
the identity steps are included in it. Otherwise the simple proof of
sequent $a^\perp\otimes b^\perp,a,b$ where $a,b$ are negative atoms,
is a case where the (only) activ!
e formula has positive subformulas in both border sequents.
Section 4.2 is unclear. Theorem 4 relies on an extension of the
"Focalization Graph method" which is left to the reader to guess,
while it would have been helpful to see it explicitly. In particular,
how are cuts treated in the so called "pre-focalization process" of
Section 3.2. The same applies to the other extension (exponentials).
Section 5 on multi-focalization only gives a direction to follow, but
no concrete result. It seems to me that multi-focalization is
interesting only if one can characterise the cases where a non
degenerate multi-focalized step can be chosen instead of the
corresponding sequence of focalized steps, without loosing
completeness.
Suggestion to improve the presentation of focalization graphs.
--------------------------------------------------------------
(for the authors but not directly relevant to committee)
Define one graph for each sequent in the positive trunk, and drop the
restriction to active formulas (I cannot see any harm in including the
inactive ones in the graph, even if in the end one only works with the
restriction of the graph to active formulas). For each sequent of the
border, the focalization graph simply links all the negative formulas
to the positive ones. Then, the focalization graphs for the inner
sequents are defined inductively top-down simply by defining how it
proceeds along the inference figure. The only interesting one is the
tensor, for which the graph of the conclusion is obtained by union of
the graphs of the premisses and identification of the vertices
corresponding to the two sub-formulas of the principal one.
-------------------- review 4 --------------------
The paper presents a generalization of Andreoli's completeness theorem
of focused proofs for MALL (theorem 2, pg.10; section 4 sketches how
to generalize theorem 2 to wider linear logic fragments). The main
improvements w.r.t. Andreoli's original theorem (here Theorem 3) are
two:
1) the authors introduce a new structure, called focalization graph
(definition 8, pg. 9), and base their proof on a geometric property of
that structure (acyclicity);
2) the problem of literals' polarity is approached with a great
freedom, allowing different polarities for different occurrences of
the same literal.
At a first reading, this approach sounds to me interesting and
promising. However I cannot evaluate positively this paper since I
found it quite inaccurate and rough (sometimes it contains real
mistakes). I guess it was written in a hurry... In order to help the
authors (and the PC) to understand what I mean for inaccuracy I write
below a short list of remarks:
pg. 2 line -3: what does it mean $\exists x.Fx$? The grammar should
set $\exists x.F$ (similarly for the universal quantifier).
pg. 3 Fig.1: the way the plus (and quantifiers) rules are written are
an example of the inaccuracy of the paper
pg.3 line +6: what do you mean with "their application is independent
from the context"? Indeed forall and with connectives have
context-sensitive rules
pg.3 line +9: "formulas built with asynchronous connectives": probably
you mean "Formulas whose most external connective is an asynchronous
one are called negative"
pg. 4 Fig. 2 where is the eigenvariable condition for the forall rule?
pg. 4 Theorem 1: "list of formulas, $\vdash \Psi, \Gamma, \Delta$"
should be "list of formulas, $\vdash ?\Psi, \Gamma, \Delta$"
pg . 4 line -6: "a simpler a shorter"....
pg. 5 line 14: "starting with the": have you said before that you
consider proofs bottom-up?; "on a formula A": adopt a more precise
terminology, for example "whose active (or principal) formula is A"
(indeed you use this terminology at page 6, line +3).
pg. 5 Proposition 1: is it right that $N$ has full permutability?
Think at the top-rule: there is a proof of the sequent $top, a \par
a$, which starts (bottom-up) with $\par$ and it ends with top, but it
doesn't exist a proof starting with $top$ AND ending with $\par$. So
by definition 1, we have not $\par / top$-permutability
pg. 6 line + 14: "produced by the rule $\alpha$", is it a standard
terminology?; "g" should be $G$
pg. 6 line -3: formulas A and F should be the same
-------------------- review 5 --------------------
The paper proposes a new proof of focalization, a truly fundamental
property of Linear Logic sequent calculus, which was
first proved by Andreoli 15 years ago.
Focalization is the key result on which are built in Linear Logic
proof-search and logic programming, for which it
was first discovered. However, focalization also justifies significant
proof-theoretical properties of Linear Logic, and -starting with recent
work by Girard- it appears more and more evident as it underlies
semantical results, in particular in Game Semantics. While Girards Ludics
is explicitly built on it, we probably still need to
better study and understand the extent and significance of focalization.
While focalization is a crucial result, it is also a very little known one:
not only the proof technique, but also the result itself are little known
even in the Linear Logic community. This is an unfortunate situation.
There are probably two reasons for this: in the original formulation,
focalization is difficult to understand as a result, and difficult to use
as a technique. Andreoli uses in fact a complex formulation of Linear
Logic, which was intended as a proof-search tool, and the proof is long,
intricate and difficult to manage.
This paper fixes this issue, by giving a proof which is simple and
modular, and by using the standard calculus.
This makes focalization accessible, and provides the community a tool both
to use and to analyze it.
The paper is well written.
The proof itself, which introduces the nice notion of focalization graph,
is compact, elegant and clear.
Moreover, it refines Andreolis original proof. In particular:
the treatments of the atoms is improved;
the modularity of the technique should allow the analysis of focalization
in extensions of the system;
working by proof transformation opens the way to study the interaction
with other transformation processes, namely cut-elimination.
This appears as a timely paper, and I recommend acceptance.