定界控制算子的范式互模拟
Normal Form Bisimulations for Delimited-Control Operators
摘要：
我们定义了一个范式双相似性的概念，无类型的按值调用λ演算扩展与定界控制操作符移位和复位。范式双相似性是一种简单、易用的行为等价关系，它将术语联系起来，而不必在所有上下文中测试它们（如上下文等价），或者将它们应用于函数参数（如应用性双相似性）。我们证明了移位和复位的范式双相似性是合理的，但不是完全的。上下文等价，我们定义了最多的技术，旨在简化互模拟证明。最后，我们说明了我们开发的技术的简单性，通过证明几个等价项。
英文摘要：
We define a notion of normal form bisimilarity for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
