概率相干空间中的微分与距离
Differentials and distances in probabilistic coherence spaces
AI总结：
本文在概率相干空间中利用态射的导数计算pPCF弱头归约的执行时间期望，并证明态射的Lipschitz性质以关联观测距离与模型距离，暗示了微分扩展的潜力。
摘要：
在概率相干空间中，作为概率函数语言的指称模型，态射是解析的，因此是光滑的。我们探讨了相应导数的两个相关应用。首先，我们展示了导数如何用于计算概率PCF（pPCF）弱头归约中执行时间的期望。其次，我们将态射的“局部”微分的一般概念应用于证明这些态射的Lipschitz性质，进而将pPCF项上的观测距离与模型自然配备的距离联系起来。这表明，以微分λ-演算的精神，将导数扩展到概率编程语言中可能具有相当的意义。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
