概率相干空间中的微分与距离
Differentials and distances in probabilistic coherence spaces
摘要:
在概率函数语言的指称模型--概率凝聚空间中,态射是解析的,因此是光滑的。我们探讨了相应衍生物的两个相关应用。首先,我们展示了如何衍生工具允许计算的执行时间的期望在弱头减少概率PCF(pPCF)。接下来,我们应用一般概念的“本地”微分态射的Lipschitz属性的证明,这些态射允许反过来将观测距离的pPCF条款的距离模型自然配备。这表明,在微分微积分的精神下,用导数扩展概率程序设计语言可能是非常有意义的。
英文摘要:
In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms 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.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。