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