Skip to Main content Skip to Navigation
Conference papers

Metric Reasoning About λ-Terms: The General Case

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 metadatas

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/hal-01639369
Contributor : Ugo Dal Lago <>
Submitted on : Monday, November 20, 2017 - 1:11:40 PM
Last modification on : Saturday, April 11, 2020 - 2:03:12 AM
Long-term archiving on: : Wednesday, February 21, 2018 - 2:24:06 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

589

Files downloads

683