Interaction graphs: multiplicatives

DOI10.1016/J.APAL.2012.04.005MaRDI QIDQ714715zbMATH OpenOpenAlexFDO

Publication date 11 October 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1205.6558

cut elimination denotational semantics geometry of interaction multiplicative linear logic operator algebras proof nets proof theory

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Semantics in the theory of computing (68Q55)

Abstract: We introduce a graph-theoretical representation of proofs of multiplicative linear logic which yields both a denotational semantics and a notion of truth. For this, we use a locative approach (in the sense of ludics) related to game semantics and the Danos-Regnier interpretation of GoI operators as paths in proof nets. We show how we can retrieve from this locative framework both a categorical semantics for MLL with distinct units and a notion of truth. Moreover, we show how a restricted version of our model can be reformulated in the exact same terms as Girard's latest geometry of interaction. This shows that this restriction of our framework gives a combinatorial approach to J.-Y. Girard's geometry of interaction in the hyperfinite factor, while using only graph-theoretical notions.

Review text

Girard's geometry of interaction (GoI) is a program that aims at giving an operative account of cut elimination by representing proofs as operators. Since the first formulation of this ambitious program, lots of refinements and developments were proposed. Some key concepts were clarified and found an accurate realization. For example, the notion of \textit{locativity}, which may be considered as being in the core of GoI since the beginning, was technically fulfilled only recently, when Girard developed Ludics: a theory of logic resting on an explicit notion of locativity [\textit{J.-Y. Girard}, Math. Struct. Comput. Sci. 11, No. 3, 301--506 (2001; Zbl 1051.03045)]. The work of T. Seiller, presented in the present article, arises when a new version of GoI (called GoI5) was proposed by \textit{J.-Y. Girard}, using advanced operator-theoretic notions, namely the hyperfinite factor in von Neumann algebras classification, in [Theor. Comput. Sci. 412, No. 20, 1860--1883 (2011; Zbl 1230.03093)]. Here, the author defines a graph-theoretical geometry of interaction for multiplicative linear logic. As in the latest version of GoI in the hyperfinite factor and in contrast to more ancient versions of GoI, the graph-theoretical GoI is developed by the author in a locative framework. In this way, the interpretation of proofs and of cut elimination is more concrete and may be an interesting setting for studying complexity. Moreover, the author's work, providing a combinatorial approach to the new concepts of GoI5, constitutes an introduction to this new version of GoI in the hyperfinite factor. The last sections of this article are devoted to this aim. Section 7 makes explicit the links between graph operations used in this graph-theoretical geometry of interaction and operator-theoretic notions used in GoI5. Section 8 describes the embedding of such graphs as operators in the hyperfinite factor. Nevertheless, this article presents above all a version of GoI which is interesting by itself. Starting from the GoI program's aim: ``To rebuild logic from a relevant notion of interacting proofs, Seiller defines a graph-theoretical framework in which a theorem of adjunction is obtained. Following the GoI program, a notion of project (a directed weighted graph on a finite set of vertices) subsumes the notion of proofs; orthogonality between projects is defined; a notion of conducts (some sets of projects which are closed by biorthogonality) subsumes the notion of formulas; finally linear constructions on conducts give the expected properties of duality to recover MLL. This version of GoI yields a denotational semantics of MLL. This result is obtained in a traditional way: by showing that a \(*\)-autonomous category may be defined from the interpretation of proofs by graphs. This proposition presents at least two interesting things: 1. While the multiplicative units have the same interpretation in most known categorical models of MLL, this is not the case in the graph-theoretical GoI. 2. This work sheds light on differences between GoI and denotational semantics as a categorical construction is obtained only at the prize of a loss of locativity. Finally, the choice of a locative setting enables the author to deepen the connections between GoI and game semantics [\textit{S. Abramsky}, \textit{P. Malacaria} and \textit{R. Jagadeesan}, Lect. Notes Comput. Sci. 789, 1--15 (1994; Zbl 0942.68615)], \textit{J. M. E. Hyland} and \textit{C.-H. L. Ong} [Inf. Comput. 163, No. 2, 285--408 (2000; Zbl 1006.68027)]. A nice application here is the possibility to define a notion of truth: a conduct is true when it contains a successful project, which would correspond to the game-semantical notion of winning strategy. Furthermore, this work allows for a better understanting of the relations between successive versions of GoI. The starting intuitions to develop this graph-theoretical GoI arise from the first version of GoI where the correctness criterion is the long-trip criterion. Choices made here are also shared with the locative approach in game semantics and with the Danos-Regnier interpretation of GoI operators as paths in proof nets [\textit{V. Danos} and \textit{L. Regnier}, Lond. Math. Soc. Lect. Note Ser. 222, 307--328 (1995; Zbl 0854.03011); Theor. Comput. Sci. 227, No. 1--2, 79--97 (1999; Zbl 0952.03008)]. Lastly, it can be seen as an interpretation in finite dimension of the latest GoI done in the hyperfinite factor.

Recommendations

Cites work

Cited in

(15)

This page was built for publication: Interaction graphs: multiplicatives

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q714715)