论文标题
概率相干空间的差速器和距离
Differentials and distances in probabilistic coherence spaces
论文作者
论文摘要
在概率相干空间中，概率功能语言的指示模型，形态是分析性的，因此平滑。我们探索相应衍生物的两个相关应用。首先，我们显示衍生产品如何允许在概率PCF（PPCF）的弱头减少中计算执行时间的期望。接下来，我们将形态的“局部”差异的一般概念应用于这些形态的Lipschitz特性的证明，允许依次将PPCF术语的观察距离与模型自然配置的距离联系起来。这表明，本着差异性lambda-calculus的精神将概率的编程语言扩展为有意义。
In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.
