一句话：将函数式程序验证中展开递归定义加SMT无量词推理的启发式，推广为组合一阶理论上的完备推理技术。
Liquid Haskell、Leon 等函数式程序自动验证工具普遍采用一种启发式：展开递归函数定义，再调用 SMT 求解器进行无量词推理。该启发式虽在实践中有效，但其理论基础、适用范围与失败原因尚不清晰。本文揭示并形式化了这一启发式背后的根本理论性质，证明它可以被推广为一种面向代数数据类型与背景理论组合的一阶推理技术；只要背景理论支持可判定的无量词推理，该方法对组合一阶理论就是完备的。这一理论既解释了启发式成功时为何有效、失败时为何失败，也刻画了用户提供的辅助信息在证明成功过程中所起的精确作用。
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.
@article{paperbot1866,
title = {Complete First-Order Reasoning for Properties of Functional Programs},
author = {Adithya Murali and Lucas Peña and Ranjit Jhala and P. Madhusudan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622835}
}