×

Zeta functions and the (linear) logic of Markov processes. (English) Zbl 07906380

Summary: The author introduced models of linear logic known as “Interaction Graphs” which generalise Girard’s various geometry of interaction constructions. In this work, we establish how these models essentially rely on a deep connection between zeta functions and the execution of programs, expressed as a cocycle. This is first shown in the simple case of graphs, before begin lifted to dynamical systems. Focussing on probabilistic models, we then explain how the notion of graphings used in Interaction Graphs captures a natural class of sub-Markov processes. We then extend the realisability constructions and the notion of zeta function to provide a realisability model of second-order linear logic over the set of all (discrete-time) sub-Markov processes.

MSC:

03B70 Logic in computer science
68-XX Computer science

References:

[1] T. Seiller Vol. 20:3 18:24 T. Seiller Vol. 20:3
[2] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59(2):543-574, 1994. doi:10.2307/2275407. · Zbl 0822.03007 · doi:10.2307/2275407
[3] Michael Artin and Barry Mazur. On periodic points. Annals of Mathematics, pages 82-99, 1965. · Zbl 0127.13401
[4] Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. The Journal of Symbolic Logic, 63(2):600-622, 1998. doi:10.2307/2586854. · Zbl 0914.03059 · doi:10.2307/2586854
[5] Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of probabilistic PCF. In Dawar and Grädel [DG18], pages 215-224. doi: 10.1145/3209108.3209187. · Zbl 1497.68331 · doi:10.1145/3209108.3209187
[6] D.L. Cohn. Measure Theory: Second Edition. Birkhäuser Advanced Texts Basler Lehrbücher. Springer New York, 2013. URL: https://books.google.dk/books?id=PEC3BAAAQBAJ. · Zbl 1292.28002
[7] Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus.
[8] In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 16:1-16:17. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.CSL.2018.16. Vol. 20:3 ZETA FUNCTIONS AND THE (LINEAR) LOGIC OF MARKOV PROCESSES 18:33 · Zbl 1528.03117 · doi:10.4230/LIPIcs.CSL.2018.16
[9] Simon Castellan and Hugo Paquet. Probabilistic programming inference via intensional semantics. In Luís Caires, editor, Programming Languages and Systems -28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 322-349. Springer, 2019. doi: 10.1007/978-3-030-17184-1_12. · Zbl 1524.68054 · doi:10.1007/978-3-030-17184-1_12
[10] Pierre-Louis Curien. Introduction to linear logic and ludics, part II. Advances in Mathematics (China), 35(1):1-44, 2006. doi:10.2307/1969645. [dAKM + 21] Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Michael Roberts. Universal semantics for the stochastic λ-calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 -July 2, 2021, pages 1-12. IEEE, 2021. doi:10.1109/LICS52264.2021.9470747. · doi:10.1109/LICS52264.2021.9470747
[11] Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput., 209(6):966-991, 2011. doi:10.1016/j.ic.2011.02. 001. · Zbl 1267.68085 · doi:10.1016/j.ic.2011.02.001
[12] Anuj Dawar and Erich Grädel, editors. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. ACM, 2018. doi: 10.1145/3209108. · Zbl 1394.03004 · doi:10.1145/3209108
[13] Vincent Danos and Russell S. Harmer. Probabilistic game semantics. ACM Trans. Comput. Logic, 3(3):359-382, jul 2002. doi:10.1145/507382.507385. · Zbl 1365.68310 · doi:10.1145/507382.507385
[14] Yoann Dabrowski and Marie Kerjean. Models of linear logic based on the schwartz ε-product. Theory and Applications of Cateogries, 34:1440-1525, 2019. · Zbl 1445.03068
[15] Thomas Ehrhard. Differentials and distances in probabilistic coherence spaces. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs. FSCD.2019.17. · Zbl 1528.68063 · doi:10.4230/LIPIcs.FSCD.2019.17
[16] Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for probabilistic PCF. J. ACM, 65(4):23:1-23:44, 2018. doi:10.1145/3164540. · Zbl 1426.68035 · doi:10.1145/3164540
[17] Boris Eng and Thomas Seiller. Multiplicative linear logic from a resolution-based tile system. 2022. arXiv:2207.08465, doi:10.48550/arXiv.2207.08465. · doi:10.48550/arXiv.2207.08465
[18] Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 309-320. ACM, 2014. doi: 10.1145/2535838.2535865. · Zbl 1284.68268 · doi:10.1145/2535838.2535865
[19] Bent Fuglede and Richard V. Kadison. Determinant theory in finite factors. Annals of Mathe-matics, 56(2), 1952.
[20] Jacob Feldman and Calvin C Moore. Ergodic equivalence relations, cohomology, and von neumann algebras. I. Transactions of the American mathematical society, 234(2):289-324, 1977. doi:10.2307/1997924. · Zbl 0369.22009 · doi:10.2307/1997924
[21] Jacob Feldman and Calvin C Moore. Ergodic equivalence relations, cohomology, and von neumann algebras. II. Transactions of the American Mathematical Society, 234(2):325-359, 1977. doi:10.2307/1997925. · Zbl 0369.22010 · doi:10.2307/1997925
[22] Jean-Yves Girard. Multiplicatives. In Lolli, editor, Logic and Computer Science : New Trends and Applications, pages 11-34, Torino, 1987. Università di Torino. Rendiconti del seminario matematico dell’università e politecnico di Torino, special issue 1987. · Zbl 0656.00005
[23] Jean-Yves Girard. Geometry of interaction II: Deadlock-free algorithms. In Proceedings of COLOG, number 417 in Lecture Notes in Computer Science, pages 76-93. Springer, 1988. doi:10.1007/3-540-52335-9_49. · Zbl 0716.03047 · doi:10.1007/3-540-52335-9_49
[24] Jean-Yves Girard. Geometry of interaction I: Interpretation of system F. In In Proc. Logic Colloquium 88, 1989. doi:10.1016/S0049-237X(08)70271-4. · doi:10.1016/S0049-237X(08)70271-4
[25] Jean-Yves Girard. Towards a geometry of interaction. In Proceedings of the AMS Conference on Categories, Logic and Computer Science, 1989. 18:34 T. Seiller Vol. 20:3
[26] Jean-Yves Girard. Geometry of interaction III: Accommodating the additives. In Advances in Linear Logic, number 222 in Lecture Notes Series, pages 329-389. Cambridge University Press, 1995. doi:10.1017/CBO9780511629150.017. · Zbl 0828.03027 · doi:10.1017/CBO9780511629150.017
[27] Jean-Yves Girard. Coherent banach spaces: A continuous denotational semantics. Theor. Comput. Sci., 227(1-2):275-297, 1999. doi:10.1016/S0304-3975(99)00056-0. · Zbl 0952.03025 · doi:10.1016/S0304-3975(99)00056-0
[28] Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3), 2001. doi:10.1007/3-540-44802-0_3. · Zbl 1051.03045 · doi:10.1007/3-540-44802-0_3
[29] Jean-Yves Girard. From foundations to ludics. Bulletin of Symbolic Logic, 9(2):131-168, Jun 2003. doi:10.2178/bsl/1052669286. · Zbl 1056.03035 · doi:10.2178/bsl/1052669286
[30] Jean-Yves Girard. Between logic and quantic : a tract, pages 346-381. Number 316 in London Mathematical Society Lecture Note Series. Cambridge University Press, 2004. doi:10.1017/ CBO9780511550850.011. · Zbl 1073.03036 · doi:10.1017/CBO9780511550850.011
[31] Jean-Yves Girard. Geometry of interaction IV: the feedback equation. In Stoltenberg-Hansen and Väänänen, editors, Logic Colloquium ’03, pages 76-117, 2006. doi:10.1017/9781316755785.006. · Zbl 1105.03064 · doi:10.1017/9781316755785.006
[32] Jean-Yves Girard. Geometry of interaction V: Logic in the hyperfinite factor. Theoretical Computer Science, 412:1860-1883, 2011. doi:10.1016/j.tcs.2010.12.016. · Zbl 1230.03093 · doi:10.1016/j.tcs.2010.12.016
[33] Jean-Yves Girard. Transcendental syntax ii: non deterministic case. Logical Methods in Com-puter Science (to appear), 2016.
[34] Jean-Yves Girard. Transcendental syntax i: deterministic case. Mathematical Structures in Computer Science, 27(5):827-849, 2017. doi:10.1017/S0960129515000407. · Zbl 1423.03248 · doi:10.1017/S0960129515000407
[35] Jean-Yves Girard. Transcendental syntax iii: equality. preprint, 2018.
[36] Masahito Hasegawa. Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi. pages 196-213. Springer Verlag, 1997. doi:10.1007/978-1-4471-0865-8_ · Zbl 1063.68599 · doi:10.1007/978-1-4471-0865-8_7
[37] John Martin Elliott Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. doi:10.1006/inco.2000.2917. · Zbl 1006.68027 · doi:10.1006/inco.2000.2917
[38] Esfandiar Haghverdi and Philip Scott. A categorical model for the geometry of interaction. Theoretical Computer Science, 350(2):252-274, 2006. doi:10.1007/978-3-540-27836-8_60. · Zbl 1086.03050 · doi:10.1007/978-3-540-27836-8_60
[39] Yasutaka Ihara. On discrete subgroups of the two by two projective linear group over p -adic fields. J. Math. Soc. Japan, 18(3):219-235, 07 1966. doi:10.2969/jmsj/01830219. · Zbl 0158.27702 · doi:10.2969/jmsj/01830219
[40] André Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. Mathemati-cal Proceedings of the Cambridge Philosophical Society, 119(3):447-468, 1996. doi:10.1017/ S0305004100074338. · Zbl 0845.18005 · doi:10.1017/S0305004100074338
[41] Marie Kerjean. A logical account for linear partial differential equations. In Dawar and Grädel [DG18], pages 589-598. doi:10.1145/3209108.3209192. · Zbl 1452.03135 · doi:10.1145/3209108.3209192
[42] Jean-Louis Krivine. Typed lambda-calculus in classical zermelo-fraenkel set theory. Archive for Mathematical Logic, 40(3):189-205, 2001. · Zbl 0990.03008
[43] Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009. · Zbl 1206.03017
[44] Alexandre Miquel. A survey of classical realizability. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications -10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 1-2. · Zbl 1218.03017
[45] Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-21691-6, doi:10.1007/ 978-3-642-21691-6_1. · Zbl 1218.03017 · doi:10.1007/978-3-642-21691-6_1
[46] Alberto Naibo, Mattia Petrolo, and Thomas Seiller. On the computational meaning of axioms. In Epistemology, Knowledge and the Impact of Interaction, pages 141-184. Springer, 2016. doi:10.1007/978-3-319-26506-3_5. · doi:10.1007/978-3-319-26506-3_5
[47] Prakash Panangaden. The category of markov kernels. Electronic Notes in Theoretical Computer Science, 22:171 -187, 1999. PROBMIV’98, First International Workshop on Probabilistic Methods in Verification. doi:10.1016/S1571-0661(05)80602-4. · doi:10.1016/S1571-0661(05)80602-4
[48] Hugo Paquet. Bayesian strategies: probabilistic programs as generalised graphical models. In Nobuko Yoshida, editor, Programming Languages and Systems -30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 -April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 519-547. Springer, 2021. doi:10.1007/978-3-030-72019-3_19. · Zbl 1473.68054 · doi:10.1007/978-3-030-72019-3_19
[49] Hugo Paquet and Glynn Winskel. Continuous probability distributions in concurrent games. In Sam Staton, editor, Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 of Electronic Notes in Theoretical Computer Science, pages 321-344. Elsevier, 2018. doi:10.1016/j.entcs.2018.11.016. · Zbl 1527.68141 · doi:10.1016/j.entcs.2018.11.016
[50] David Ruelle. Zeta-functions for expanding maps and anosov flows. Inventiones mathematicae, 34(3):231-242, 1976. doi:10.1007/BF01403069. · Zbl 0329.58014 · doi:10.1007/BF01403069
[51] Thomas Seiller. Interaction graphs: Multiplicatives. Annals of Pure and Applied Logic, 163:1808-1837, December 2012. doi:10.1016/j.apal.2012.04.005. · Zbl 1252.03143 · doi:10.1016/j.apal.2012.04.005
[52] Thomas Seiller. Logique dans le facteur hyperfini : géometrie de l’interaction et com-plexité. PhD thesis, Université Aix-Marseille, 2012. URL: http://tel.archives-ouvertes. fr/tel-00768403/.
[53] Thomas Seiller. Towards a complexity-through-realizability theory. 2015. URL: http://arxiv. org/abs/1502.01257, arXiv:1502.01257.
[54] Thomas Seiller. Interaction graphs: Additives. Annals of Pure and Applied Logic, 167:95 -154, 2016. doi:10.1016/j.apal.2015.10.001. · Zbl 1433.03148 · doi:10.1016/j.apal.2015.10.001
[55] Thomas Seiller. Interaction graphs: Full linear logic. In IEEE/ACM Logic in Computer Science (LICS), 2016. URL: http://arxiv.org/pdf/1504.04152.
[56] Thomas Seiller. Interaction graphs: Graphings. Annals of Pure and Applied Logic, 168(2):278-320, 2017. doi:10.1016/j.apal.2016.10.007. · Zbl 1422.03131 · doi:10.1016/j.apal.2016.10.007
[57] Thomas Seiller. A correspondence between maximal abelian sub-algebras and linear logic fragments. Mathematical Structures in Computer Science, 28(1):77-139, 2018. doi:10.1017/ S0960129516000062. · Zbl 1456.03105 · doi:10.1017/S0960129516000062
[58] Thomas Seiller. Interaction graphs: Non-deterministic automata. ACM Trans. Comput. Log., 19(3):21:1-21:24, 2018. doi:10.1145/3226594. · Zbl 1407.68193 · doi:10.1145/3226594
[59] Thomas Seiller. Interaction Graphs: Exponentials. Logical Methods in Computer Science, Volume 15, Issue 3, August 2019. doi:10.23638/LMCS-15(3:25)2019. · Zbl 1509.03168 · doi:10.23638/LMCS-15(3:25)2019
[60] Thomas Seiller. Mathematical informatics, 2024. Habilitation thesis. URL: https://theses. hal.science/tel-04616661.
[61] Thomas Seiller, Luc Pellissier, and Ulysse Léchine. On the power of euclidean division. lower bounds for algebraic machines, semantically. https://hal.archives-ouvertes.fr/ hal-01921942, 2024.
[62] Audrey Terras. Zeta functions of graphs: a stroll through the garden, volume 128. Cambridge University Press, 2010. doi:10.1017/CBO9780511760426. · doi:10.1017/CBO9780511760426
[63] Kazushige Terui. Computational ludics. Theor. Comput. Sci., 412(20):2048-2071, 2011. doi: 10.1016/j.tcs.2010.12.026. · Zbl 1222.03032 · doi:10.1016/j.tcs.2010.12.026
[64] Jaap Van Oosten. Realizability: an introduction to its categorical side. Elsevier, 2008. · Zbl 1225.03002
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.