We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state. Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence. However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that reach bounded configurations but can potentially have unbounded call stacks and input an unbounded number of unknown functions from their context. Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content. We embody this in a stackless Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined. To enhance the effectiveness of our bisimulation, we develop up-to techniques and confirm their soundness for PDNF Bisimulation. We develop a prototype implementation of our technique which is able to verify equivalence in examples from practice and the literature that were out of reach for previous work.

翻译：我们提出下推范式双模拟（Pushdown Normal Form Bisimulation，PDNF Bisimulation）来验证具有局部状态的高阶函数式编程语言中的上下文等价性。与先前关于范式双模拟（Normal Form Bisimulation，NF Bisimulation）的工作类似，PDNF双模拟在上下文等价性下既是可靠的也是完备的。然而，与传统NF双模拟不同，PDNF双模拟对于一类能达到有界配置但可能具有无界调用栈并从其上下文输入无界数量未知函数的程序项而言，还是可判定的。我们的方法基于以下原理：在可达性模型检验中，下推系统可以由设计为接受其初始/最终栈内容的有限状态自动机来模拟。我们通过一个无栈的带标号转移系统（Labelled Transition System，LTS）以及一种用于调用栈的即时饱和过程来具体实现这一点，并在此基础上定义双模拟关系。为增强我们双模拟方法的有效性，我们开发了上至技术（up-to techniques）并确认其在PDNF双模拟中的可靠性。我们实现了所提技术的原型系统，能够验证实际和文献中先前工作无法企及的示例中的等价性。