# Metric Reasoning About $\lambda$-Terms: The General Case (Long Version)

## TL;DR

This paper explores the properties of context distance in probabilistic lambda calculi, extending analysis beyond affine cases, and introduces pseudometrics that are fully abstract for call-by-name and call-by-value settings.

## Contribution

It provides a comprehensive analysis of context distance in probabilistic lambda calculi, including trivialization conditions, coinductive characterizations, and fully abstract pseudometrics.

## Key findings

- Characterizes when context distance trivializes.
- Defines coinductive, tuple-based distance in $ ext{Lambda}^ ext{oplus}_!$.
- Derives and proves full abstraction of pseudometrics for probabilistic lambda calculi.

## 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 $\lambda$-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 $\Lambda^\oplus_!$. We finally derive pseudometrics for call-by-name and call-by-value probabilistic $\lambda$-calculi, and prove them fully-abstract.