Metric Reasoning About $λ$-Terms: The General Case (Long Version)

Abstract

In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of \emph{metrics} rather than equivalences or partial orders. This holds, in particular, for probabilistic higher-order programs. A natural notion of comparison, then, becomes context distance, the metric analogue of Morris' context equivalence. In this paper, we analyze the main properties of the context distance in fully-fledged probabilistic $λ$-calculi, this way going beyond the state of the art, in which only affine calculi were considered. We first of all study to which extent the context distance trivializes, giving a sufficient condition for trivialization. We then characterize context distance by way of a coinductively defined, tuple-based notion of distance in one of those calculi, called $Λ^\oplus_!$. We finally derive pseudometrics for call-by-name and call-by-value probabilistic $λ$-calculi, and prove them fully-abstract.