Step-Indexed Logical Relations for Probability (long version)

TL;DR

This paper develops step-indexed logical relations for a higher-order probabilistic programming language, enabling sound reasoning about program equivalences, including features like polymorphism, recursion, and state.

Contribution

It introduces a novel logical relation framework for probabilistic languages with advanced features, extending to stateful constructs while maintaining reasoning effectiveness.

Findings

Logical relation is sound and complete with respect to the contextual preorder.

The framework effectively reasons about program equivalences involving probability and state.

The extended relation handles dynamically allocated references in probabilistic contexts.

Abstract

It is well-known that constructing models of higher-order probabilistic programming languages is challenging. We show how to construct step-indexed logical relations for a probabilistic extension of a higher-order programming language with impredicative polymorphism and recursive types. We show that the resulting logical relation is sound and complete with respect to the contextual preorder and, moreover, that it is convenient for reasoning about concrete program equivalences. Finally, we extend the language with dynamically allocated first-order references and show how to extend the logical relation to this language. We show that the resulting relation remains useful for reasoning about examples involving both state and probabilistic choice.