概率保护λ演算中马氏链的关系推理
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
摘要：
我们扩展了简单类型的保护$λ$ -演算与离散概率，并赋予它一个程序逻辑的保护概率计算的关系属性的推理。这提供了一个框架的编程和推理的无限随机过程，如马尔可夫链。我们证明了逻辑的声音，解释其判断的拓扑结构的树，并通过使用概率耦合的语义分布在离散类型的关系断言。程序逻辑被设计为支持关系细化类型风格的语法导向证明，但保留了用离散分布扩展的高阶逻辑的表达能力，以及对具有不同类型或语法结构的表达式进行关系推理的能力。此外，我们的证明系统利用耦合文献中的一个著名定理来证明概率表达式的关系推理的更好的证明规则。我们用广泛的例子来说明这些好处，这些例子超出了以前系统的范围，包括随机游走之间的移位耦合和块耦合。
英文摘要：
We extend the simply-typed guarded $λ$-calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic computations. This provides a framework for programming and reasoning about infinite stochastic processes like Markov chains. We demonstrate the logic sound by interpreting its judgements in the topos of trees and by using probabilistic couplings for the semantics of relational assertions over distributions on discrete types. The program logic is designed to support syntax-directed proofs in the style of relational refinement types, but retains the expressiveness of higher-order logic extended with discrete distributions, and the ability to reason relationally about expressions that have different types or syntactic structure. In addition, our proof system leverages a well-known theorem from the coupling literature to justify better proof rules for relational reasoning about probabilistic expressions. We illustrate these benefits with a broad range of examples that were beyond the scope of previous systems, including shift couplings and lump couplings between random walks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
