Upper approximating probabilities of convergence in probabilistic coherence spaces

TL;DR

This paper introduces a probabilistic coherence space model with an extensional structure to approximate convergence probabilities of probabilistic PCF programs, using polynomial approximations from an extended language.

Contribution

It develops a novel probabilistic coherence space framework with an extensional structure and an adapted Krivine Machine for polynomial approximations of convergence probabilities.

Findings

Polynomial approximations provide bounds from below and above.

Extension of language with an error symbol enables maximal extensionality.

Model effectively approximates probabilities of convergence in probabilistic PCF.

Abstract

We develop a theory of probabilistic coherence spaces equipped with an additional extensional structure and apply it to approximating probability of convergence of ground type programs of probabilistic PCF whose free variables are of ground types. To this end we define an adapted version of Krivine Machine which computes polynomial approximations of the semantics of these programs in the model. These polynomials provide approximations from below and from above of probabilities of convergence; this is made possible by extending the language with an error symbol which is extensionally maximal in the model.