[Prev][Next][Index][Thread]
Paper ann.: A Calculus of Order and Interaction
Hello,
a paper on a simple calculus for commutative/non-commutative linear
logic is available. It has an intuitive concurrency semantics, and it
is obtained by distillation of a few basic "physical" principles.
Readers of "types" may be interested in the novel cut-elimination
proof presented in the paper.
The paper is available from CoRR
<http://xxx.lanl.gov/abs/cs/9910023>
or (in color) from the page
<http://pikas.inf.tu-dresden.de/~guglielm/paper.html>
Enjoy,
Alessio Guglielmi
Department of Computer Science - Dresden University of Technology
Hans-Grundig-Str. 25 fax +49 (351) 463 8342
D-01062 Dresden - Germany
-----------------------------------------------------------------
A Calculus of Order and Interaction
Alessio Guglielmi
System MV is a simple, propositional linear calculus that deals with
the commutative as well as the non-commutative composition of
structures. The multiplicative fragment of linear logic is a special
case of MV, and the tensor rule does not suffer from unnecessary
non-determinism in context partitioning as it does in the sequent
calculus of linear logic. System MV is obtained by breaking the
symmetry in a formal system that is symmetric in the top-down vs.
bottom-up building of derivations. A cut elimination theorem is the
direct consequence of this break in the symmetry. The formal systems
presented in this paper act on structures intermediate between proof
nets and sequents. Connectives disappear, giving place to structural
relations between atoms: as a result, there are no logical rules in
MV, all the rules are structural. Structures are not decomposed in
their main connectives, rather they freely move and interleave
respecting order. Interaction happens when structures that are dual
through negation come into close communication. The rules in MV
result from enforcing a small set of basic conservation laws, making
the design of the calculus as little arbitrary as possible, and
indeed very natural in the perspective of the concurrent management
of information. The calculus of structures can naturally embrace
classical and linear logic, and allows to prove cut elimination
properties on atomic versions of the cut rule.
64 pages. Submitted to the Journal of the ACM.