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.
翻译:作者引入了称为“ 互动图” 的线性逻辑模型, 该模型概括了 Girard 的各种交互构造几何结构。 在这项工作中, 我们确定这些模型如何基本上依赖于 zeta 函数与程序执行之间的深层联系, 以双周期的形式表达。 这首先在简单的图表中显示, 然后再开始向动态系统升格。 聚焦于概率模型, 然后我们解释“ 互动图” 中使用的图形概念如何捕捉到亚 Markov 过程的自然类别 。 然后我们扩展了真实性构建和 zeta 函数的概念, 以提供一个二阶线性逻辑模型, 而不是所有( 不稳定时间) 子Markov 过程的可变性模型 。