
Noncommutative 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 noncommutative linear logic, which combines two kinds of multiplicative connectives: the noncommutatives and the commutatives. The link between them is made by new modalities: the mobilities.
Introduction
Syntax.
We introduce a noncommutative version of Girard's multiplicative linear logic [2]. We consider
two kinds of multiplicative connectives: the noncommutatives ? and +, and the commutatives ?
and }; and two modalities, the mobilities ? and ffl. As in Abrusci's pure noncommutative 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 multifunctoriality 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 noncommutative 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 cutelimination for the multiplicative fragment (with commutatives, noncommutatives and mobilities). The result for the whole logic would likely rely on a proofnet syntax, which is under development.
Pure noncommutative 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)).
References
[1] M. Abrusci. Phase semantics and sequent calculus for pure noncommutative 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.
Appendix
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 inferiorequivalent 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.
Notations.
Let i and j be contractible orderings on disjoint domains, and k a contractible subordering 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.
Rules.
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
Noncommutatives
` ?; 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
Mobilities
` ?; 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
Multiplicatives
` ?; 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]
Exponentials
` ?; 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]
Additives
` ?; A [i] ` ?; B [ifB=Ag]
` ?; A&B [ifA&B=Ag]
` ?; A [i]
` ?; A?B [ifA ?B=Ag]
` ?; B [i]
` ?; A? B [ifA ?B=Bg]
Constants
` 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