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.
翻译:作者引入了称为“交互图”的线性逻辑模型,这些模型推广了吉拉德的多种几何交互构造。在本研究中,我们揭示了这些模型本质上是建立在ζ函数与程序执行之间的深层联系之上,这种联系以余循环的形式表达。首先在简单图的情形中展示这一结果,随后将其推广至动力系统。聚焦于概率模型,我们进一步阐释了交互图中使用的图概念如何捕捉一类自然的子马尔可夫过程。随后,我们扩展了可实现性构造与ζ函数的概念,以在所有(离散时间)子马尔可夫过程的集合上构建二阶线性逻辑的可实现性模型。