限界控制操作的正常形式双模拟
摘要：无类型按值调用lambda演算（untyped call-by-value lambda calculus）的正常形式（normal form）等价被定义为扩展了定界控制操作符shift和reset的行为等价。正常形式等价是一种简单、易于使用的行为等价，它将项与所有上下文进行测试（如上下文等价）或将其应用于函数参数（如应用等价）相关联。我们证明了shift和reset的正常形式等价在上下文等价方面是正确而不完全的，并定义了目标技术，旨在简化等价证明。最后，我们通过证明几个项的等价来说明我们开发的技术的简单性。
作者：Dariusz Biernacki, Serguei Lenglet
论文ID：1202.5959
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-02-29