paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Zeta Functions and the (Linear) Logic of Markov Processes

Zeta 函数与马尔可夫过程的(线性)逻辑
LMCS vol.Volume 20, Issue 32024匹配度 3/10 · 论文属于概率编程与线性逻辑的形式语义研究,仅与概率/贝叶斯程序分析有较间接的理论关联;未涉及静态分析、LLM/Agent、浮点程序分析或工业落地,因此与当前研究画像匹配度低。引用 0 inbox
Thomas Seiller
crossref: 2026-09-10

AI 速览

一句话:揭示 Zeta 函数与程序执行的 cocycle 联系,并为 sub-Markov 过程建立二阶线性逻辑模型。

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

问题
线性逻辑的 Interaction Graphs 模型如何与程序执行建立深层结构联系,并如何推广到概率/马尔可夫过程?
方法
通过 Zeta 函数与 cocycle 建立程序执行表示,把 graphings 与 sub-Markov 过程对应,并扩展可实现性构造与 Zeta 函数。
评估
以理论构造与证明为主,从图推广到动力系统,再在离散时间 sub-Markov 过程上建立可实现性模型;不涉及实验评估。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2731,
  title = {Zeta Functions and the (Linear) Logic of Markov Processes},
  author = {Thomas Seiller},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 20, Issue 3},
  year = {2024},
  doi = {10.46298/lmcs-20(3:18)2024}
}