Lambda项规范化中的约简策略及其对堆使用的影响
摘要：高阶对象的表示，如程序、证明、公式和类型，对于许多符号计算任务都非常重要。支持这种表示的系统通常依赖于某种类型的λ-演算术语的内部视图的实现。已经提出了各种各样的λ-术语表示法，以明确地处理替换作为实现这种表示的基础。然而，在实际的规约策略中有几种选择。最常见的策略仅通过递增使用环境而隐含地使用这些表示法。这种方法不允许更小的替换步骤与λ-术语上的其他感兴趣的操作交织在一起。然而，使用这些表示法的朴素策略也可能很昂贵：每次使用替换传播规则都会在堆上创建一个新的结构，而这个结构在紧接着的步骤中通常会被丢弃。因此，在这两种方法之间存在一个权衡。本论文描述了这两种方法的实际实现，基于此讨论了它们的权衡，并最终提出了一种综合方法，该方法利用重写规则应用中的递归，并在必要时挂起替换操作。
作者：Xiaochu Qi
论文ID：cs/0405075
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23