一句话:证明离散锥上的概率稳定函数可视为广义幂级数,并将概率相干空间嵌入连续概率模型 Cstabm。
本文研究可测锥与可测稳定函数构成的范畴 Cstabm,它是带连续概率与完全递归的高阶语言的指称模型。作者从离散概率视角考察该模型,构造一个笛卡尔闭、全且忠实的函子,将概率相干空间——带完全递归与离散概率的高阶语言的完全抽象指称模型——嵌入 Cstabm。证明的关键是推广实分析中的 Bernstein 定理,从而把离散锥之间的稳定函数刻画为广义幂级数。该结果说明离散概率模型可被视为连续概率模型的特例,并揭示了稳定函数与幂级数表示之间的深层联系。
We study the category Cstabm of measurable cones and measurable stable functions---a denotational model of an higher-order language with continuous probabilities and full recursion [7]. We look at Cstabm as a model for discrete probabilities, by showing the existence of a cartesian closed, full and faithful functor which embeds probabilistic coherence spaces---a fully abstract denotational model of an higher language with full recursion and discrete probabilities [8]---into Cstabm. The proof is based on a generalization of Bernstein's theorem from real analysis allowing to see stable functions between discrete cones as generalized power series.
DOI 原文 ·
@inproceedings{paperbot4371,
title = {Probabilistic Stable Functions on Discrete Cones are Power Series},
author = {Raphaëlle Crubillé},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209198}
}