paperbot · PL 论文追踪

全部论文 待读 收藏

P2 An Algebraic Theory of Markov Processes

马尔可夫过程的代数理论
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文是概率程序与马尔可夫过程的纯代数语义基础,虽与概率/贝叶斯编程语义有理论关联,但未涉及用户核心关注的 PL+AI、静态分析、LLM/Agent、浮点程序分析等方向,也缺乏工程实现与工业落地。引用 15 inbox
Giorgio Bacci, Radu Mardare, Prakash Panangaden, Gordon Plotkin
crossref: 2026-09-12

AI 速览

一句话:用定量等式逻辑与单子组合,给出离散/连续状态空间马尔可夫过程的代数公理化。

论文研究马尔可夫过程的代数公理化问题。马尔可夫过程是概率迁移系统的基本模型,也是概率程序的底层语义。作者采用定量等式逻辑(quantitative equational logic)作为框架,并使用 Hyland 等人关于单子组合的工作,以结构化的方式给出理论:将刻画 Kantorovich 度量的插值重心代数(interpolative barycentric algebras)与收缩算子理论相结合。由此得到离散和连续状态空间下马尔可夫过程所需的公理化。该工作不仅具有自身理论意义,也表明一般性的效应组合概念可推广到定量情形。

问题
如何为作为概率迁移系统与概率程序语义的马尔可夫过程提供代数公理化,并覆盖离散与连续状态空间。
方法
在定量等式逻辑中,结合单子组合、插值重心代数(刻画 Kantorovich 度量)与收缩算子理论来构造公理化。
评估
通过给出离散和连续状态空间的公理化,并讨论效应组合到定量框架的推广来体现理论结果。
原文摘要(Abstract)

Markov processes are a fundamental model of probabilistic transition systems and are the underlying semantics of probabilistic programs. We give an algebraic axiomatisation of Markov processes using the framework of quantitative equational logic introduced in [13]. We present the theory in a structured way using work of Hyland et al. [9] on combining monads. We take the interpolative barycentric algebras of [13] which captures the Kantorovich metric and combine it with a theory of contractive operators to give the required axiomatisation of Markov processes both for discrete and continuous state spaces. This work apart from its intrinsic interest shows how one can extend the general notion of combining effects to the quantitative setting.

链接与引用

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

BibTeX
@inproceedings{paperbot4313,
  title = {An Algebraic Theory of Markov Processes},
  author = {Giorgio Bacci and Radu Mardare and Prakash Panangaden and Gordon Plotkin},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209177}
}