Full abstraction for probabilistic PCF

TL;DR

This paper introduces a probabilistic extension of PCF with a denotational semantics based on probabilistic coherence spaces, establishing full abstraction and observational equivalence for the language.

Contribution

It develops a probabilistic version of PCF with a novel semantics that achieves full abstraction, linking operational and denotational perspectives.

Findings

The probabilistic PCF language is fully abstract with respect to the model.

The semantics accurately captures observational equivalence.

The language combines call-by-name and call-by-value evaluation strategies.

Abstract

We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if the language is globally call-by-name, we allow a call-by-value evaluation for ground type arguments in order to provide the language with a suitable algorithmic expressiveness. We describe a denotational semantics based on probabilistic coherence spaces, a model of classical Linear Logic developed in previous works. We prove an adequacy and an equational full abstraction theorem showing that equality in the model coincides with a natural notion of observational equivalence.