定界控制算子的应用互模拟
Applicative Bisimulations for Delimited-Control Operators
摘要：
我们开发了一个行为理论的无类型调用的值λ演算扩展与定界控制操作符的移位和复位。对于这个演算，我们讨论了可能的可观察到的行为，我们定义了一个适用的双相似性，其特征在于上下文等价。然后，我们比较了应用的双相似性和CPS等价，一个关系的控制算子的研究中经常使用的术语。在这个过程中，我们说明了如何双相似性可以用来证明与定界控制效果的条款等价。
英文摘要：
We develop a behavioral theory for the untyped call-by-value lambda calculus extended with the delimited-control operators shift and reset. For this calculus, we discuss the possible observable behaviors and we define an applicative bisimilarity that characterizes contextual equivalence. We then compare the applicative bisimilarity and the CPS equivalence, a relation on terms often used in studies of control operators. In the process, we illustrate how bisimilarity can be used to prove equivalence of terms with delimited-control effects.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
