Strong Adequacy and Untyped Full-Abstraction for Probabilistic Coherence Spaces

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.