1: \begin{abstract}

2:   Randomized higher-order computation can be seen as being captured by

3:   a $\lambda$-calculus endowed with a single algebraic operation,

4:   namely a construct for binary probabilistic choice. What matters

5:   about such computations is the \emph{probability} of obtaining any

6:   given result, rather than the \emph{possibility} or the

7:   \emph{necessity} of obtaining it, like in (non)deterministic

8:   computation. Termination, arguably the simplest kind of reachability

9:   problem,  can be spelled out in at least two ways, depending on

10:   whether it talks about the probability of convergence or about the

11:   expected evaluation time, the second one providing a stronger

12:   guarantee. In this paper, we show that intersection types are

13:   capable of precisely characterizing \emph{both} notions of

14:   termination inside \emph{a single} system of types: the probability

15:   of convergence of any $\lambda$-term can be underapproximated by its

16:   \emph{type}, while the underlying derivation's \emph{weight} gives a

17:   lower bound to the term's expected number of steps to normal

18:   form. Noticeably, both approximations are tight---not only soundness

19:   but also completeness holds.  The crucial ingredient is

20:   non-idempotency, without which it would be impossible to reason on

21:   the expected number of reduction steps which are necessary to

22:   completely evaluate any term. Besides, the kind of approximation we

23:   obtain is proved to be \emph{optimal} recursion theoretically: no

24:   recursively enumerable formal system can do better than that.

25: \end{abstract}