Differentials and distances in probabilistic coherence spaces

TL;DR

This paper investigates derivatives in probabilistic coherence spaces, demonstrating their use in computing execution time expectations and establishing Lipschitz properties, which could enhance probabilistic programming languages.

Contribution

It introduces the application of derivatives in probabilistic coherence spaces to compute expectations and prove Lipschitz properties, linking observational and model distances.

Findings

Derivatives enable expectation computation of execution time.

Lipschitz property of morphisms is established.

Model and observational distances are related.

Abstract

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.