Abstract We consider the probabilistic untyped lambda-calculus and prove a stronger form of the adequacy property for probabilistic coherence spaces (PCoh), showing how the denotation of a term statistically distributes over the denotations of its head-normal forms. We use this result to state a precise correspondence between PCoh and a notion of probabilistic Nakajima trees, recently introduced by Leventis in order to prove a separation theorem. As a consequence, we get full abstraction for PCoh. This latter result has already been mentioned as a corollary of Clairambault and Paquet’s full abstraction theorem for probabilistic concurrent games. Our approach allows to prove the property directly, without the need of a third model.

Abstract In this paper we present an operational semantics for the ‘call-by-name’ probabilistic λ-calculus, whose main feature is to use only deterministic relations and to have no constraint on the reduction strategy. The calculus enjoys similar properties to the usual λ-calculus. In particular we prove it to be confluent, and we prove a standardisation theorem.

We study the notion of observational equivalence in the call-by-name probabilistic λ-calculus, where two terms are said observationally equivalent if under any context, their head reductions converge with the same probability. Our goal is to generalise the separation theorem to this probabilistic setting. To do so we define probabilistic Böhm trees and probabilistic Nakajima trees, and we mix the well-known Böhm-out technique with some new techniques to manipulate and separate probability distributions.