AI 中文总结
研究概率程序中由遗忘对手控制不确定性的推理问题，引入opOL逻辑，基于结果逻辑和概率分离逻辑建模，为随机和非确定性结果分析及证明终止性提供规则，经案例研究测试表现力并在Lean 4中实现机械化。
AI 中文摘要
在概率程序的背景下，遗忘对手在不查看随机抽取结果的情况下解决不确定性。遗忘性是在线算法和分布式协议中的常见假设，但随机抽取与对手选择之间的复杂交互使得正确性推理具有挑战性。虽然在结合随机化与不确定性的程序推理方面取得了重大进展，但大多数工作都集中在自适应模型上，其对程序状态的全知视图对于某些类别的程序来说过于强大，无法确立正确性。我们引入了遗忘概率结果逻辑（opOL），这是一种用于推理由遗忘对手控制不确定性的概率程序的新逻辑。基于结果逻辑和概率分离逻辑，opOL将对手选择建模为一种资源，并使用概率独立性来确保随机结果对对手隐藏。opOL证明系统为随机和非确定性结果的案例分析以及证明几乎必然终止提供了富有表现力和组合性的规则。通过包括分页算法和领导者选举协议在内的几个案例研究测试了其表现力。opOL元理论和案例研究在Lean 4中实现了机械化。
英文摘要
In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.
