Skip to Main content Skip to Navigation
New interface
Conference papers

Metric Reasoning About λ-Terms: The General Case

Raphaëlle Crubillé 1, 2 Ugo Dal Lago 1, 3 
Abstract : In any setting in which observable properties have a quantitative flavor, 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 pseudomet-rics for call-by-name and call-by-value probabilistic λ-calculi, and prove them fully-abstract.
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Ugo Dal Lago Connect in order to contact the contributor
Submitted on : Monday, November 20, 2017 - 1:11:40 PM
Last modification on : Tuesday, September 6, 2022 - 1:27:29 PM
Long-term archiving on: : Wednesday, February 21, 2018 - 2:24:06 PM


Files produced by the author(s)



Raphaëlle Crubillé, Ugo Dal Lago. Metric Reasoning About λ-Terms: The General Case. ESOP 2017 - 26th European Symposium on Programming, Apr 2017, Uppsala, Sweden. pp.341-367, ⟨10.1007/978-3-662-54434-1_13⟩. ⟨hal-01639369⟩



Record views


Files downloads