一句话：在概率相干空间中用导数刻画 pPCF 执行时间期望，并证明态射 Lipschitz 性以连接观测距离与模型距离。
概率相干空间是概率函数式语言的指称模型，其态射为解析且光滑。本文研究该模型导数的两个应用。首先，利用导数计算概率 PCF（pPCF）在弱头归约下执行时间的期望，从而把微分结构用于资源/复杂度分析。其次，将态射的“局部”微分概念用于证明这些态射的 Lipschitz 性质，并据此把 pPCF 项上的观测距离与该模型自然携带的距离联系起来。结果表明概率相干空间的微分不仅可刻画执行代价，还能控制程序行为距离，暗示按微分 lambda 演算的思路扩展概率编程语言具有意义。
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.