[Prev][Next][Index][Thread]

on polarities and linear logic

Date: Fri, 6 Dec 91 17:56:59 +0100
To: linear@cs.stanford.edu

			ON THE SEX OF ANGELS

			jean-yves girard


	I will try to present the syntax and semantics (in terms of phase
semantics) of polarities ; as we shall see, the main twist is that additives
are handled in a completely new way : plus becomes a more complex connective
whereas with becomes simpler. The big problem with additives is distributivity
which forces one to make dubious additive contractions. In some sense distribu-
tivity of par over with will be now wrong.
	Obviously this calculus is more complex than the existing one : 
however one may say that :
i) the semantics is nice (ordered rings)
ii) one can still do familiar linear logic : it suffices to restrict one
to sequents /- gamma ; (for instance we still get distributivity as
/- (Aperp par Bperp) with (Aperp par Cperp), A times (B plus C) ; what fails
is the stronger form where the central comma is replaced by ;).  From the
viewpoint of the user what is presented here can be seen as a more primitive
language.
iii/-  the ultimate criterion will be whether or not proof-nets do improve, but
this is not to-day's problem.
	A last point about phase semantics : i do not consider it as a very
important approach, but only as a way to give the ultimate checkup ; i already
had the main lines of this calculus, but it was not always clear what restrictions
should be made for certain rules (the typical restriction being that the focus
is empty) ; the semantics did it for me ; for instance up to a few days i believed
that (c)S can be ignored when S is of behaviour -c, but the semantics refused
to do this for me and the rule which removes (c) has an empty 'pi'. The semantics
refused on the other hand to help me define an affine and a pertinent conjunction
which however make sense on denotational terms ; this is why the styles a and p 
are absent here.


I THE SYNTAX : FORMULAS

	As usual the connectives go by pairs : 0/true, 1/bottom, times/par,
plus/with, thereis/forall, !/?, up/down ; there are atoms in each behaviour
+l -l +c -c (styles a and p are not considered).
We define classes of formulas P and C (P positive, C subclass of P correspon-
ding to +c) ; the negations N and S of thes classes are implicitely part
of the definition
P = p/c/upN/!P/PtimesP/PplusP/thereisP/O/1
C = c/!P/CtimesC/CplusC/thereisC/0/1
	As we see it, connectives are defined only on some polarities ; but
the transexuel operations up and down enable one to define them everywhere. In
this way linear logic appears as defined logic inside.
ATTENTION : when translating the shriek of LL in our system, we have to
use !updownP instead of the expected !P : this accounts for the fact 
noticed by andreoli-pareschi that focalisation is destroyed when one crosses
a bang. For us losing focalisation is the replacement of P by updownP, a
process reminiscent of double negation. In other terms the system we present
is the true intuitionistic linear logic, and the familiar one is related
to it through a king of notnot translation.

II THE SEMANTICS : FACTS

	Let R be a commutative ring with unit u and zero z ; we assume
that R is ordered and R+ is the set of positive elements, so R+ is closed
under finite products and sums so u and z are in R+. 
	We fix also a subset Bot of R ; we require that Bot+ is closed
under finite sums hence z belongs to Bot. Let Raf be the set of affine maps
>from R to itself, i.e. maps a.x+b. R+ is canonically embedded into Raf
(identify a with a homothety a.x). So we can define for any subset X of Raf
its positive part X+ by intersecting it with R+). We define orthogonality of
two objects a and b of Raf as follows : at least one of them, say a,  must be 
in R+ ; in that case applying the other to must lead to an element of Bot 
(so b(a) belongs to Bot). For any set X we define Xperp as the set of all x 
such that xX is included in Bot. All sets will be subsets of Raf.
	If X is positive i.e. X = X+, we define cl(X) to be Xperpperp+ ; cl(.)
is obviously idempotent, and we can therefore introduce positive facts as
the sets of the form cl(X) (equivalently Yperp+) : they satisfy P = cl(P) ;
positive facts contain z, but may fail to be closed under sum : this will
account for our limited acceptation of distributivity at the logical level.
	Negative facts are the perps of positive sets (equivalently of positive
facts). Their positive part is closed under arbitrary sums.
	
III INTERPRETATION OF CONNECTIVES
	
UpN is just N+ ; observe that UpN is closed under sum, and this is why
distributivity will hold in some sense. DownP is defined by duality.
PtimesQ is presented as the closure of P.Q ; NparM is defined by duality
PplusQ is presented as the closure of P+Q (the set of sums not the union!) ;
observe that NwithM is not the intersection of N and M, although this holds
when we restrict to positive parts.
O and 1 are the respective closures of z and u.
!P is defined as the closure of those z in P such that z belongs to the fact 1
and z = z.z ; should we need affine or pertinent shrieks it would be enough
to retain only one of these two extra conditions.
	Finally, a fact C is of behaviour +c when it is positive and such
that C is included in updown!C ; very easy to show that the judgements of
behaviour +c of I above are sound wrt this definition. One may ask why adding
updown in front : this is simply because +c is closed under plus ; imagine
that i want to prove that !C plus !D is included in !(C plus D) : i would need
that the sum of idempotents is idempotent ; hence i prove the inclusion of
the two updowns (my weaker formulation) ; but since updown(P plus Q) is equal
to updown(P union Q) (consequence of (N with M)+ = N+ inter M+), i can replace
updown(P plus Q) by P union Q.

IV SEQUENT CALCULUS
	
	New features : a room for a distinguished formula that may or may
not be occupied by a positive formula (the stoup in my reference [2], but
also the focus of Andreoli-Pareschi : i propose to keep their terminology) ;
the use of (c) as hypocrisy for ? ; the use of + as hypocrisy for with.
	A prime sequent is of the form /- gamma ; or /- gamma ; P  where
gamma is a multiset of formulas and expressions (c)N. A sequent is any
finite sum of prime sequents with two important details
- if the summands are gamma_i;p_i then all p_i are equal ; using distributivity
we shall write our sequents as /- gamma; or /gamma;P
- we have to be very cautious about the problem of identity of formulas :
when i write two occurences of A are they equal or just variants ? A way
to see that is to think that there are parcels of formulas. This is essential
when we use a decomposition gamma = gamma'.delta + delta' which involves
distributivity : it should respect the parcels.
	To each formula (for Comrade Brezhnev : given facts of the right
behaviours for the atoms) A i associate a fact [A] with the same behaviour
in the obvious way. A sequent /- gamma; is sound if the following holds
choose for each A occuring an element of [Aperp]+ for each (c)N occuring
an element of [!Nperp]+ ; WHEN IN THE SAME PARCEL CHOOSE THE SAME ELEMENT.
Then the result of forming the algebraic expression suggested by gamma belongs
to Bot. The same for a sequent /- gamma ; P except that the result should
now belong to [P].
	We now list the rules which are sound

		IDENTITY/NEGATION

i) the identity axioms /- Pperp;P
ii) the Pcut-rule : from /- gamma;P and /- delta.Pperp+delta';pi derive
/-delta.gamma+delta';pi
iii) the Ncut-rule : from /-gamma.N; and /-delta.Nperp+delta';pi derive
/-delta.gamma+delta';pi
iv) the Ccut-rule : from /- (c)gamma;P and /-delta.(c)Pperp+delta';pi derive
/-delta.(c)gamma+delta';pi ; the noation (c)gamma is short hand to say that
we have here a prime sequent made of expressions (c)A.

		STRUCTURE

i) rules for sums : the null sequent z as axiom, the rule : from /- gamma;
and /- gamma'; derive /- gamma+gamma';
ii) parcel rule :from /- gamma;pi derive /- gamma';pi/-  by putting two parcels
together
iii) from /- gamma+delta;pi derive /- gamma.(c)N+delta;pi
>from /- gamma.(c)N.(c)N+delta;pi derive /- gamma.(c)N+delta;pi
iv) from /- gamma.(c)S; derive /- gamma.S; S must be of behaviour -c ; observe that
the focus is empty and that there is no 'delta' like say in iii) ; this is because
of the way +c is defined semantically. 

		LOGIC

i) axiom /-1 ; from /- gamma+delta;pi derive /- gamma.Bottom+delta;pi 
ii) from  /- gamma;P and /-delta;Q derive /- gamma.delta;PtimesQ
This rule creates parcels when we develop the product gamma.delta using
distributivity.
iii) from /- gamma.N.M+delta;pi derive/- gamma.NparM+delta;pi
iv) axiom   /- gamma.True;pi
v) from  /- gamma;P and /-delta;Q derive /- gamma+delta;PplusQ
vi) from /- gamma.(N+M)+delta;pi derive/- gamma.NwithM+delta;pi
vii) from /- (c)gamma;P derive /- (c)gamma;!P
viii) from /-delta.(c)N+delta';pi derive /-delta.?N+delta';pi 
ix) from /- gamma.N; derive /-gamma;UpN
x) from /- gamma;P derive /- gamma.DownP;

	There is no problem in stating a soundness result.


V COMPLETENESS

	First of all we can define the product of prime sequents as follows
/-gamma;pi . /-delta;pi' = /gamma.delta;pi.pi' when one of pi pi' is empty
zero otherwise.  Of course we treat here the (c)P as idempotents ie we
do not count multiplicities of such expressions in prime sequents. 
This is easily understood if we compare the semantic definition of !P
and the shriek introd rule.
Then the set of all formal algebraic sums forms a ring R.
Then we form Bot as the set consisting of
- all provable sequents /-gamma;pi
- all elements of R which are not legal sequents ; we denote this by R~
	To any positive formula P i associate [P] a positive fact : the set
of contexts /-gamma; such that /-gamma;P is provable.
	To any negative formula N i associate [N] a negative fact : the set 
of all functions /-gamma.x+delta;pi such that /-gamma.N+delta;pi is provable
(when i write N i mean any one of the infinitely many variants of N, hence
neither gamma nor delta may have negative coefficients) together with those 
functions such that /-gamma.M+delta;pi fails to be a sequent for an appropriate
choice of M. 
	Then one must prove the obvious things ; note that Down[P] is the set 
of all contexts /-gamma;pi such that /-gamma,P;pi is provable.


VI AN EXAMPLE

/- (Aperp par Bperp) with (Aperp par Cperp);A times (B plus C)  is not 
provable ; one easily gets
/-(Aperp.Bperp)+(Aperp.Cperp); A times (B plus C) but the factorisation is
impossible since the two Aperps are in the same parcel.
In order to prove the weaker form
/- (Aperp par Bperp) with (Aperp par Cperp), A times (B plus C);
one proves
/-(Aperp.Bperp),A times (B plus C); and
/-(Aperp~.Cperp),A times (B plus C);
and sum them. Since the two Aperps are distinct (in different parcels)
par-introd can be applied. 
	The restriction about identity is again nothing unatural, and
is caused by the fact that . does not distributes over + when we deal
with subsets (typically ideals) in a ring. 

VII PROOF-NETS

	This should be the next mail ; just one remark about how things
now look different
a negative sequent (with empty focus) should be represented as a net
whose conclusions are those of the sequent AND an additional one
for the symbol ';'
a positive sequent (with non-empty focus) should be represented as
a net whose conclusions are those of the sequent ; among them a distinguished
one, the focused formula.
	In both cases the net has a distinguished formula ; this can
be used to connect weakenings on Bottom ; but the most spectacular is
on plus and with ; the with comes from the reconciliation of two formulas
separated by a +. Such + are created by the plus rule (sum of contexts)
or the structural rule of sum ; in both cases the two subnets are tied
together by the focus, empty or not.