Skip to Main content Skip to Navigation
New interface
Conference papers

The Space of Interaction

Beniamino Accattoli 1 Ugo Dal Lago 2 Gabriele Vanoni 2 
1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Randomized higher-order computation can be seen as being captured by a λ-calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of obtaining any given result, rather than the possibility or the necessity of obtaining it, like in (non)deterministic computation. Termination, arguably the simplest kind of reachability problem, can be spelled out in at least two ways, depending on whether it talks about the probability of convergence or about the expected evaluation time, the second one providing a stronger guarantee. In this paper, we show that intersection types are capable of precisely characterizing both notions of termination inside a single system of types: the probability of convergence of any λ-term can be underapproximated by its type , while the underlying derivation’s weight gives a lower bound to the term’s expected number of steps to normal form. Noticeably, both approximations are tight—not only soundness but also completeness holds. The crucial ingredient is non-idempotency, without which it would be impossible to reason on the expected number of reduction steps which are necessary to completely evaluate any term. Besides, the kind of approximation we obtain is proved to be optimal recursion theoretically: no recursively enumerable formal system can do better than that.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03346767
Contributor : Ugo Dal Lago Connect in order to contact the contributor
Submitted on : Sunday, September 19, 2021 - 11:59:29 AM
Last modification on : Thursday, January 20, 2022 - 5:30:13 PM

File

2104.13795.pdf
Files produced by the author(s)

Identifiers

Citation

Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The Space of Interaction. LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2021, Rome, France. pp.1-13, ⟨10.1109/LICS52264.2021.9470726⟩. ⟨hal-03346767⟩

Share

Metrics

Record views

46

Files downloads

47