The geometry of multiplicatives and additives: interaction and orthogonality

Etienne Duchesne

Description

Niveau: Supérieur, Doctorat, Bac+8
The geometry of multiplicatives and additives: interaction and orthogonality Etienne Duchesne Laboratoire d'Informatique Fondamentale, University of Aix-Marseille, CNRS, 4 april 2011 Abstract We present a denotational semantics of multiplicative linear logic based on the geometry of interaction. In that semantics, we can define polymorphism using a construction similar to the one of history-free game semantics. We can also present the standard longtrip criterion of proof-nets as an orthogonality relation in the sense of Hyland and Schalk [HS03], and build a category of orthogonality which provides a fully complete model of MLL (without mix). Besides we extend these constructions – polymorphism and orthogonality –, to the inter- pretation of additive connectives. 1 Introduction The proof-nets and proof-structures for multiplicative linear logic [Gir87a], are quite standard syntactical objects. Given a MLL formula, a proof-structure is just defined by a pairing of dual literals in the formula, indicating which literals are linked by the axioms. The distinction between proof-structures and proof-nets – i.e. between pairings coming from proofs and the others – has originally been expressed using the longtrip criterion, based on a notion of paths in the proof- structures. For each connective of the formula, we choose the paths walking through it, i.

• agent


• interaction


• logic based


• between incoming


• define ?


• also extend


• been showed

Sujets

• Duchesne
• Interaction

Informations

• Publié par: mijec
• Nombre de lectures: 37
• Langue: English

Extrait

1

The

geo

metry of multiplicatives and additives: interaction and orthogonality

Etienne Duchesne Laboratoire d’Informatique Fondamentale, University of Aix-Marseille, CNRS, [e-mail]

4 april 2011

Abstract We present a denotational semantics of multiplicative linear logic based on the geometry of interaction. In that semantics, we can define polymorphism using a construction similar to the one of history-free game semantics. We can also present the standard longtrip criterion of proof-nets as an orthogonality relation in the sense of Hyland and Schalk [HS03], and build a category of orthogonality which provides a fully complete model of MLL (withoutmix). Besides we extend these constructions – polymorphism and orthogonality –, to the inter- pretation of additive connectives.

Introduction

The proof-nets and proof-structures for multiplicative linear logic [Gir87a], are quite standard syntactical objects. Given a MLL formula, a proof-structure is just defined by a pairing of dual literals in the formula, indicating which literals are linked by the axioms. The distinction between proof-structures and proof-nets – i.e. between pairings coming from proofs and the others – has originally been expressed using the longtrip criterion, based on a notion of paths in the proof- structures. For each connective of the formula, we choose the paths walking through it, i.e. we determine a one-to-one correspondence between incoming edges and outgoing edges of each connective. Such an orientation of connectives is called a switching (the different possibilities are given in figure 1). Then a pairing of an MLL formula is actually a proof-net when for any such switching of connectives, the walk it defines is a unique big cycle: a longtrip. The very first version of the geometry of interaction [Gir87b] gives a computational content to the longtrip criterion. It reformulates the pairings of a proof-structures and the switchings as permutations over the occurrences of literals in the formula. A pairing is then a symmetry, exchanging the linked literals, while a switching is a the permutation of literals which is defined by the paths from literals to literals. The longtrip criterion is then reformulated as acyclicitycriterion: the symmetry defined by a pairing comes from a proof-net if and only if for any permutation induced by a switching, the composition of that symmetry with this permutation is cyclic. Geometry of interaction gives also a semantical account of cut-elimination. The interpretation of a proof-net is a symmetry on a finite set representing the literals of the conclusion formula; then the composition of two interpretations is defined by the interaction of these two permutations on the common occurences of literals they are sharing through the cut formula. The result of the interaction is the permutation which to a literal which does not belong to the cut formula, applies alternatively the two composed permutations until the result does not belong to the cut formula. This procedure, expressed by Girard as theexecution formula, is equivalent to the definition of a trace [JSV96] in a monoidal category. Actually the whole definition of geometry of interaction has been presented as a construction on traced monoidal categories [AJ94b, AHS02] – the so-called Intconstruction of Joyalet al..

1

Many works have been related to the geometry of interaction since its introduction. If we had to, we could try to distinguish different groups amongst them. Some works have defined extensions of geometry of interaction to other fragments of linear logic, or to other specific models. For instance it has been extended towards exponentials [Gir89] and additives [Gir95]. It has also been reformulated as a computation of paths in proof-nets [DR95], or as a token machine [Lau01]. These extensions usually does not provide a denotational semantics, and it is important to remark that the presentation of the longtrip criterion in these extended framework fails, mainly because cyclicity can be expressed only in finite structures, while exponentials introduced the possibility of an infinite behaviour. Since the seminal work of Abramskyet al.categorical definition of geometry of in-on the teraction, a whole branch of categorical semantics deals with the study of theIntconstruction. For instance it has been showed that semi-biproducts are preserved by this construction [HK09], leading to the construction of models of MALL. The possiblity to define a typed interpretation thanks toIntconstruction is also deeply studied [HS05, Hag06, HS10]. Eventually history-free game semantics [AJ94a, HhLO93] is related to the geometry of inter- action in the sense that the choice function on moves is more or less the GoI interpretation. So game semantics is very close to a particular model of GoI, but it provides denotational semantics and supports categorical presentations. And indeed several important full completeness results have been proved in that framework.

The present paper belongs to the last group of works, even if it doesn’t deal with game seman- tics. Our objective is to redefine the original geometry of interaction for MLL and the original longtrip criterion in a denotational framework. What we obtain is very close to an history-free game semantics in which any reference to player or opponent has been canceled. The objects of our model define associations between some sets of positions and finite sets of token – just as games define associations between plays and moves. The morphisms are then defined both as a relation on positions, and as a permutation on token. This definition provides a degenerated model of MLL based on the principle that interaction defines composition. Then we introduce polymorphism using a construction reminiscent of domain theory, which also appears in history-free game semantics [AJ94a, HhLO93]. We can then show that the elements of the model which belongs to a polymorph type correspond exactly to a lax notion of copy-cat: they are generated by the permutations of propositional variables. With a slight modification of the model, we can present the longtrip criterion as an orthogo- nality relation in sense of Hyland and Schalk [HS03]. The modification is actually inspired by the last version of geometry of interaction [Gir08, Sei11] in which morphisms keep a trace of past in- teractions. The orthogonality category we obtained is rich enough to interpret the counter-proofs: the elements of the model which are induced by the switchings of a formula Γ actually belong to the interpretation of Γ ⊥ define the interaction against the switchings of proof-nets. So we can inside the model. We obtain then a full completeness result for MLL withoutmix. All these constructions – category of interaction, polymorphism, orthogonality – are then extended to the case of additives. The interpretation of additives is based on an indexation of positions, each index representing a copy of an additive slice. But unlike the GoI of additives defined by Girard [Gir95], the elements of that model can perform permutations of occurrences of literalsbetween additive slicesliberality allows us to define a longtrip as a cyclic permutation. This  over slices. And indeed the notion of polymorphism and orthogonality can be extended without difficulties to the additive case. We can also extend the definition of switching to the additives, by allowing also paths between slices. It provides again the possiblity to interpret the counter-proofs of a formula Γ in its dual Γ ⊥ ; however there is no completeness result to expect as there is no correctness criterion of MALL based on longtrip. The omitted proofs can be found in appendix.

2