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