递归程序的自动期望值分析
摘要：基于自然编程构造，如过程、局部变量和递归，我们研究了在概率程序中完全自动推断预期结果值。尽管关键，但捕捉这些结构变得非常复杂。关键贡献是定义了一个术语表示，称为infer[.]，将预期语义转换为一阶约束，可通过标准方法自动化。关键步骤是使用逻辑变量，受到先前关于递归程序的Hoare逻辑的工作的启发。值得注意的是，我们的方法不限于尾递归，可以用迭代替代，不需要额外的见解。我们在原型ev-imp中实现了这种分析。我们提供了充分的实验证据，证明了原型算法的表达能力。
作者：Martin Avanzini and Georg Moser and Michael Schaper
论文ID：2304.01284
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-26