Non-commutative linear logic with mobilities

Paul Ruet

LIENS, Ecole Normale Sup?erieure, 45 rue d'Ulm, 75005 Paris, France

Email: ruet@dmi.ens.fr

Abstract
We introduce a new version of non-commutative linear logic. We consider two kinds of multiplicative connectives: the non-commutatives and the commutatives. The link between them is made by new modalities: the mobilities. We give a sequent calculus for this logic, and we prove cut-elimination. The first motivation for this new approach was the semantics of concurrent processes, specifically that of concurrent constraint programs.

Introduction

Syntax.
We introduce a non-commutative version of Girard's multiplicative linear logic [2]. We consider two kinds of multiplicative connectives: the non-commutatives ? and +, and the commutatives ? and }; and two modalities, the mobilities ? and ffl. As in Abrusci's pure non-commutative linear logic[1], there are two negations: the left one ?: and the right one :?, such that ?(A?) = A and (?A)? = A. They are defined by De Morgan laws, which express the duality between ? and +, ? and }, ? and ffl.

The link between the two kinds of multiplicatives is made by the mobilities ? and ffl, through the isomorphisms ?A ? ?B ?= ?(A ?B), and dually fflA + fflB ?= ffl(A}B). This is to parallel with the fundamental isomorphisms !A?!B ?=!(A&B) and ?A}?B ?=?(A ? B) of commutative linear logic. These formulas are made into a logic thanks to a sequent calculus.

The mobilities enjoy the usual rules of dereliction and promotion, expressing multi-functoriality and (co-)monadicity (A ` fflA a` ffl ffl A and dually ? ? A a` ?A ` A).

These formulas are made into a logic thanks to a sequent calculus.

Sequent calculus.
Formulas are first equiped with a polarity: plain A (just written A) and parenthesized A, written (A). The distinction between parenthesized formulas and not parenthesized ones is similar to the distinction between the classical and linear parts in sequents of Unified Logic [3]: (A) is a hypocrisy for fflA. This distinction is necessary in our non-commutative version, whereas it is not absolutely essential in commutative linear logic.

Sequents are contractible (partial) orders indexed by formulas (in the style of the ordered sequents of Retor?e [4]). We give a sequent calculus for this logic, and we prove cut-elimination.

Pure non-commutative linear logicis a subsystem of ours, where the only authorized formulas are ? and +. Constants can be easily accomodated.

Our first motivation for this new approach was a semantics of concurrent processes, specifically that of concurrent constraint programs [5], and the need for a `sequential' connective (Retor?e's before connective < is not a solution, because A ? (B < C) ` B < (A ?C)).

References

[1] M. Abrusci. Phase semantics and sequent calculus for pure non-commutative classical linear logic. Journal of Symbolic Logic, 56(4), 1991.

[2] J.Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.

[3] J.Y. Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201{217, 1993.

[4] Ch. Retor?e. R?eseaux et s?equents ordonn?es. PhD thesis, Universit?e Paris 7, 1993.

[5] V.A. Saraswat. Concurrent constraint programming. ACM Doctoral Dissertation Awards. MIT Press, 1993.