Metric Reasoning About λ-Terms: The General Case

Raphaëlle Crubillé 1, 2 Ugo Dal Lago 1, 3
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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 : Friday, January 4, 2019 - 5:33:38 PM
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

367

Files downloads

58