Adequacy for Predicate Transformer Semantics
TL;DR
This paper establishes a generic framework to prove adequacy for predicate transformer semantics with respect to an appropriately designed operational semantics, and covers a wide range of instances, including total expected costs, cost moments, conditional expectations, and expected multiplicative rewards of probabilistic higher-order programs with unbounded recursion.
Abstract
Verifying effectful higher-order programs, such as probabilistic programs with unbounded recursion, is a central problem in program verification. Predicate transformer semantics, closely related to continuation-passing style and weakest precondition semantics, has been proposed as a compositional method for computing verification objectives. Due to its categorical and denotational formulation, it can uniformly capture quantitative properties such as expected costs. However, its relationship to operational semantics remains largely unexplored with respect to more advanced properties, such as cost moments and conditional expectations of probabilistic programs with unbounded recursion, thereby leaving its connection to concrete program executions unclear. In this paper, we establish a generic framework to prove adequacy for predicate transformer semantics with respect to an appropriately designed operational semantics. Our approach is simple yet expressive enough to cover a wide range of instances, including total expected costs, cost moments, conditional expectations, and expected multiplicative rewards of probabilistic higher-order programs with unbounded recursion.