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中实现了该分析，并通过大量实验验证了该原型算法表达能力。