2017/01/19 by Raphaëlle Crubillé, Crubillé, Raphaëlle, Ugo Dal Lago +1
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1701.05521
openalex publication_date 2017/01/19 · openalex created_date 2022/10/02 · openalex updated_date 2026/07/28
In any setting in which observable properties have a quantitative flavour, it is natural to compare computational objects by way of 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 Λ^⊕_!. We finally derive pseudometrics for call-by-name and call-by-value probabilistic λ-calculi, and prove them fully-abstract.