×

zbMATH — the first resource for mathematics

Interaction graphs: additives. (English) Zbl 1433.03148
Summary: Geometry of Interaction (GoI) is a research program initiated by Jean-Yves Girard which aims at defining a semantics of linear logic proofs accounting for the dynamical aspects of cut elimination. We present here a parametrised construction of a Geometry of Interaction for Multiplicative Additive Linear Logic (MALL) in which proofs are represented by families of directed weighted graphs. Contrarily to former constructions dealing with additive connectives [J.-Y. Girard, Lond. Math. Soc. Lect. Note Ser. 222, 329–389 (1995; Zbl 0828.03027); Theor. Comput. Sci. 412, No. 20, 1860–1883 (2011; Zbl 1230.03093)], we are able to solve the known issue of obtaining a denotational semantics for MALL by introducing a notion of observational equivalence. Moreover, our setting has the advantage of being the first construction dealing with additives where proofs of MALL are interpreted by finite objects. The fact that we obtain a denotational model of MALL relies on a single geometric property, which we call the trefoil property, from which we obtain, for each value of the parameter, adjunctions. We then proceed to show how this setting is related to Girard’s various constructions: particular choices of the parameter respectively give a combinatorial version of his latest GoI [Zbl 1230.03093], a refined version of older Geometries of Interaction [J.-Y. Girard, Stud. Logic Found. Math. 127, 221–260 (1989; Zbl 0686.03030); Lect. Not. Comput. Sci. 417, 76–93 (1990; Zbl 0716.03047); Zbl 0828.03027], and even a generalisation of his multiplicatives [J.-Y. Girard, in: Convegno su logic and computer science: new trends and applications. Torino: Rosenberg & Sellier. 11–33 (1987; Zbl 0667.03046)] construction. This shows the importance of the trefoil property underlying our constructions since all known GoI constructions to this day rely on particular cases of it.

MSC:
03F52 Proof-theoretic aspects of linear logic and other substructural logics
03F05 Cut-elimination and normal-form theorems
68Q55 Semantics in the theory of computing
PDF BibTeX Cite
Full Text: DOI arXiv
References:
[1] Abramsky, S.; Haghverdi, E.; Scott, P. J., Geometry of interaction and linear combinatory algebras, Math. Structures Comput. Sci., 12, 5, 625-665, (2002) · Zbl 1014.03056
[2] Abramsky, S.; Jagadeesan, R., New foundations for the geometry of interaction, Inform. and Comput., 111, 1, 53-119, (1994) · Zbl 0803.03014
[3] Asperti, A.; Danos, V.; Laneve, C.; Regnier, L., Paths in the lambda-calculus. three years of communications without understanding, (Symposium on Logic in Computer Science, 1994. LICS ’94. Proceedings, 4-7 Jul 1994, (1994)), 426-436
[4] Aubert, C.; Seiller, T., Characterizing co-NL by a group action, Math. Structures Comput. Sci., (2014), available on CJO2014 · Zbl 1362.68084
[5] Aubert, C.; Seiller, T., Logarithmic space and permutations, Inform. and Comput., (2014), to appear
[6] Danos, V., La logique linéaire appliquée à l’étude de divers processus de normalisation (principalement du λ-calcul), (1990), Paris VII University, Ph.D. thesis
[7] Danos, V.; Regnier, L., Local and asynchronous beta-reduction (an analysis of Girard’s execution formula), (Proceedings of the Eighth Annual Symposium on Logic in Computer Science, LICS ’93, Montreal, Canada, June 19-23, 1993, (1993), IEEE Computer Society), 296-306
[8] Danos, V.; Regnier, L., Proof-nets and the Hilbert space, (Proceedings of the Workshop on Advances in Linear Logic, (1995), Cambridge University Press New York, NY, USA), 307-328 · Zbl 0854.03011
[9] Fuglede, B.; Kadison, R. V., Determinant theory in finite factors, Ann. of Math., 56, 2, (1952) · Zbl 0046.33604
[10] Girard, J.-Y., Linear logic, Theoret. Comput. Sci., 50, 1, 1-101, (1987)
[11] Girard, J.-Y.; Lolli, Multiplicatives, Logic and Computer Science: New Trends and Applications, Università di Torino, Torino, 1987, Rend. Semin. Mat. Univ. Politec. Torino, 11-34, (1987)
[12] Girard, J.-Y., Geometry of interaction II: deadlock-free algorithms, (Proceedings of COLOG, Lecture Notes in Computer Science, vol. 417, (1988), Springer), 76-93
[13] Girard, J.-Y., Geometry of interaction I: interpretation of system F, (Proc. Logic Colloquium ’88, (1989)), 221-260
[14] Girard, J.-Y., Towards a geometry of interaction, (Proceedings of the AMS Conference on Categories, Logic and Computer Science, (1989)), 69-108
[15] Girard, J.-Y., Geometry of interaction III: accommodating the additives, (Advances in Linear Logic, Lecture Notes Series, vol. 222, (1995), Cambridge University Press), 329-389 · Zbl 0828.03027
[16] Girard, J.-Y., Light linear logic, (Selected Papers from the International Workshop on Logical and Computational Complexity, LCC ’94, (1995), Springer-Verlag London, UK), 145-176
[17] Girard, J.-Y., Proof nets: the parallel syntax for proof theory, (Ursini, A., Logic and Algebra, Lecture Notes in Pure and Applied Mathematics, vol. 180, (1995), M. Dekker)
[18] Girard, J.-Y., Locus solum: from the rules of logic to the logic of rules, Math. Structures Comput. Sci., 11, 3, (2001) · Zbl 0999.68545
[19] Girard, J.-Y., Between logic and quantic: a tract, (Linear Logic in Computer Science, London Mathematical Society Lecture Note Series, vol. 316, (2004), Cambridge University Press), 346-381 · Zbl 1073.03036
[20] Girard, J.-Y., Geometry of interaction IV: the feedback equation, (Stoltenberg-Hansen, Väänänen, Logic Colloquium ’03, (2006)), 76-117 · Zbl 1105.03064
[21] Girard, J.-Y., Geometry of interaction V: logic in the hyperfinite factor, Theoret. Comput. Sci., 412, 1860-1883, (2011) · Zbl 1230.03093
[22] J.-Y. Girard, La syntaxe transcendantale, manifeste, 2011.
[23] Girard, J.-Y., Normativity in logic, (Dybjer, P.; Lindström, S.; Palmgren, E.; Sundholm, G., Epistemology Versus Ontology, Logic, Epistemology, and the Unity of Science, vol. 27, (2012), Springer), 243-263 · Zbl 1314.03051
[24] Gonthier, G.; Abadi, M.; Lévy, J.-J., The geometry of optimal lambda reduction, (Sethi, R., POPL, (1992), ACM Press), 15-26
[25] Krivine, J.-L., Typed lambda-calculus in classical Zermelo-fraenkel set theory, Arch. Math. Logic, 40, (2001) · Zbl 0990.03008
[26] Lamping, J., An algorithm for optimal lambda calculus reduction, (Allen, F. E., POPL, (1990), ACM Press), 16-30
[27] Malacaria, P.; Regnier, L., Some results on the interpretation of lambda-calculus in operator algebras, (Proceedings of the Sixth Annual Symposium on Logic in Computer Science, LICS ’91, Amsterdam, The Netherlands, July 15-18, 1991, (1991), IEEE Computer Society), 63-72
[28] Seiller, T., Interaction graphs: multiplicatives, Ann. Pure Appl. Logic, 163, 1808-1837, (December 2012)
[29] Seiller, T., Logique dans le facteur hyperfini : géometrie de l’interaction et complexité, (2012), Université Aix-Marseille, Ph.D. thesis
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.