Paper ann.: A Calculus of Order and Interaction


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
or (in color) from the page


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.