一句话:揭示 Zeta 函数与程序执行的 cocycle 联系,并为 sub-Markov 过程建立二阶线性逻辑模型。
论文研究线性逻辑的 Interaction Graphs 模型及其与程序执行的关系。作者首先在图的情形下揭示 Zeta 函数与程序执行之间存在由 cocycle 表达的深层联系,随后将该观点提升到动力系统。针对概率模型,论文说明 Interaction Graphs 中的 graphing 概念自然刻画了一类 sub-Markov 过程。进一步,作者扩展可实现性构造与 Zeta 函数概念,在所有离散时间 sub-Markov 过程的集合上给出二阶线性逻辑的可实现性模型。该工作把几何交互、Zeta 函数与概率过程统一起来,为线性逻辑的语义与概率计算提供了新框架。
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.