page 1  (4 pages)
2to next section

Non-commutative linear logic with mobilities

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


We introduce a new version of non-commutative linear logic, which combines two kinds of multiplicative connectives: the non-commutatives and the commutatives. The link between them is made by new modalities: the mobilities.


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.

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). Constants are easily accomodated.

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]). In a sequent ` ? [i], i denotes the order and ? the multiset of indexing formulas.

We give a sequent calculus for this logic, and we prove cut-elimination for the multiplicative fragment (with commutatives, non-commutatives and mobilities). The result for the whole logic would likely rely on a proof-net syntax, which is under development.

Pure non-commutative linear logic is a subsystem of ours, where the only authorized formulas are ? and +. 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)).


[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.


Contractible orderings.
Let i be a finite partial ordering. Its domain is denoted d(i). Following Retor?e [4], we define two relations between elements x and y of d(i): x is said equivalent to y, written x ?i y, if they have the same predecessors and the same successors; x is said inferior-equivalent to y, written x -i y, if x is the only predecessor of y (equivalently if y is the only successor of x).

If x ?i y, ifx?y=x; yg is the result of identifying x and y in i and then naming the new element x ? y. Similarly if x -i y, ifx ? y=x; yg is the result of identifying x and y in i and then naming the new element x ? y. These two operations on orderings are said contractions, and an ordering is said contractible if it can reduce to a singleton via a finite sequence of contractions. The formula indexing the singleton is then denoted bi.
Contractibility is preserved by contractions.

Let i and j be contractible orderings on disjoint domains, and k a contractible sub-ordering of i. ifj=kg is the ordering on (d(i) n d(k)) [ d(j) defined by: ifj=kg ?d(i)nd(k)= i ?d(i)nd(k); ifj=kg ?d(j)= j; for x 2 d(i)nd(k) and y 2 d(j), x ifj=kg y iff x i some element in d(k); and for x 2 d(j) and y 2 d(i)nd(k), x ifj=kgy iff some element in d(k) i y.

Let i and j be contractible orderings on disjoint domains. i [ j denotes the ordering on d(i) [d(j) defined by: i [ j ?d(i)= i, i [ j ?d(j)= j, and that is all. i OE j denotes the ordering on d(i) [ d(j) obtained by asserting each element in d(i) less than each element in d(j).

ifj=kg, i [ j and i OE j are contractible.

In the following, we should speak of occurrences of formulas instead of formulas. To avoid these complications, we adopt the convention that all our formulas are distinct (for instance by adding extra indices, like in the typed >=-calculus; when necessary we will even make explicit use of indices).

The rules of the sequent calculus are:

Axiom / Cuts

` A?;A [A? OE A] ` ?; A [i] ` ?; A? [j] (?)
` ?; ? [k]

` ?; (A) [i] ` (?); A? [j] (?)
` ?; (?) [k]

(?) : A? initial in j and k = if(j n fA?g)=Ag, or A final in i and k = jf(i n fAg)=A?g


` ?; A [i] ` ?; B [j] (??)
` ?; ?; A?B [k]

` ?; A; B [i] A -i B
` ?; A+B [ifA +B=A;Bg]

(??) : B initial in j and k = if(jfA ?B=Bg)=Ag, or A final in i and k = jf(ifA ?B=Ag)=Bg


` ?; A [i]
` ?; (A) [if(A)=Ag]

` ?; (A) [i] A comparable to all elements of i
` ?; fflA [iffflA=(A)g]

` ?; (A); (B) [i] (? ? ?)
` ?; (A); (B) [j]

` (?); A [i] A comparable to all elements of i
` (?); ?A [if?B=Bg]

(? ? ?) : A -i B and A ?j B, or A ?i B and A -j B


` ?; A [i OE fAg] ` ?; B [j OE fBg]
` ?; ?; A? B [(i [ j) OE fA ?Bg]
` ?; A [fAg OE i] ` ?; B [fBg OE j]
` ?; ?; A?B [fA ? Bg OE (i [ j)]

` ?; A; B [i] A ?i B
` ?; A}B [ifA}B=A; Bg]

` ?; (A); (B) [i] A ?i or -i B
` ?; (A}B) [if(A}B)=A; Bg]


` ?; A [i]
` ?; ?A [if?A=Ag]

` ?; ?Ax; ?Ay [i] ?Ax ?i?Ay
` ?; ?A [if?A=?Ax; ?Ayg]

` ? [i]
` ?; ?A [i [ f?Ag]

`??; A [i] i is a flat order, with A initial or final
`??; !A [if!A=Ag]


` ?; A [i] ` ?; B [ifB=Ag]
` ?; A&B [ifA&B=Ag]
` ?; A [i]
` ?; A?B [ifA ?B=Ag]
` ?; B [i]
` ?; A? B [ifA ?B=Bg]


` i [;] (no rule for 1) ` ?; > [i] (> comparable to all elements of i)

` ? [i] y
` ?; e [j]

` ? [i]
` ?; ? [i ?j f?g] (no rule for 0)

(y) : j ??= i and e comparable to all elements of j