Pruning Simply Typed Lambda-Terms
Pruning Simply Typed Lambda-Terms
复制标题
修剪简单类型的 Lambda 术语
DOI：
10.1093/logcom/6.5.663
复制
发表时间：
1996
影响因子：
0.7
通讯作者：
S. Berardi
中科院分区：
文献类型：
--
作者：
S. Berardi
我们说一个简单类型的λ-项是另一个简单类型的λ-项的“修剪”，如果前者是通过用伪常数替换某些子项而从后者获得的。我们证明了“修剪”保留了一个简单类型的λ-项的观察行为，如果它不修改的类型，也没有上下文（类型的自由变量的分配）的长期。该结果用于定义映射Fl：{简单类型化的λ-项} → {简单类型化的λ-项}，以移除函数程序中的冗余代码。在本文的其余部分，我们证明了一些性质Fl有趣的从计算的角度来看。计算Fl的算法包括在附录中。
We say that a simply typed λ-term is a ‘pruning’ of another one if the former is obtained from the latter by replacing some subterms with dummy constants. We prove that ‘pruning’ preserves observational behaviour of a simply typed λ-term if it does not modify the type nor the context (assignment of types to free variables) of the term. This result is used to define a map Fl: {simply typed λ-terms} → {simply typed λ-terms} removing redundant code in functional programs. In the rest of the paper we prove some property of Fl interesting from a computational viewpoint. An algorithm to compute Fl is included in the Appendix.