Full abstraction for probabilistic PCF
Logic in Computer Science
2015-11-05 v1
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.
Keywords
Cite
@article{arxiv.1511.01272,
title = {Full abstraction for probabilistic PCF},
author = {Thomas Ehrhard and Michele Pagani and Christine Tasson},
journal= {arXiv preprint arXiv:1511.01272},
year = {2015}
}