一句话：提出通用框架证明谓词转换器语义相对于操作语义的充分性，覆盖无界递归概率高阶程序。
验证带效应的高阶程序（如无界递归概率程序）是程序验证的核心问题。谓词转换器语义与CPS及最弱前置条件语义密切相关，可作为组合式方法计算验证目标，并统一捕捉期望代价等定量性质，但其与操作语义的关系，特别是对代价矩、条件期望等高级性质，尚缺乏研究。本文建立一个通用框架，证明谓词转换器语义相对于专门设计的操作语义的充分性。该框架简单且表达力强，可覆盖全期望代价、代价矩、条件期望以及期望乘性奖励等实例，从而为无界递归概率高阶程序的定量性质提供语义基础。
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.
@article{WatanabeIK26,
title = {Adequacy for Predicate Transformer Semantics},
author = {Kazuki Watanabe and Mirai Ikebuchi and Mayuko Kori},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828674}
}