In this work, we study the fully automated inference of expected result values of probabilistic programs in the presence of natural programming constructs such as procedures, local variables and recursion. While crucial, capturing these constructs becomes highly non-trivial. The key contribution is the definition of a term representation, denoted as infer[.], translating a pre-expectation semantics into first-order constraints, susceptible to automation via standard methods. A crucial step is the use of logical variables, inspired by previous work on Hoare logics for recursive programs. Noteworthy, our methodology is not restricted to tail-recursion, which could unarguably be replaced by iteration and wouldn't need additional insights. We have implemented this analysis in our prototype ev-imp. We provide ample experimental evidence of the prototype's algorithmic expressibility.

翻译：本文研究在存在过程、局部变量和递归等自然编程结构的情况下，概率程序期望结果值的全自动推断方法。虽然这些结构至关重要，但对其进行有效建模却极具挑战性。本文的核心贡献在于定义了一种称为infer[.]的项表示方法，该方法将预期望语义转化为一阶约束，从而可通过标准方法实现自动化。关键步骤在于引入逻辑变量，这一思路受先前关于递归程序霍尔逻辑研究的启发。值得关注的是，我们的方法不限于尾递归——这类递归完全可用迭代替代且无需额外洞见。我们已在原型系统ev-imp中实现了该分析，并通过大量实验证明了原型系统在算法表达能力方面的有效性。