Sharing in the Weak Lambda-Calculus
Sharing in the Weak Lambda-Calculus
复制标题
弱 Lambda 演算中的共享
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Luc Maranget
中科院分区：
文献类型：
--
作者：
Tomasz Blanc;J. Lévy;Luc Maranget
尽管在λ-演算中有几十年的研究，但弱λ-演算的句法性质并没有得到很大的关注。然而，这个理论比通常的强λ-演算理论更适合于编程语言的实现。事实上，弱显式替换、计算单子、带let语句的λ演算、超级组合子等框架都是为了与编程语言实现相关的特殊目的而开发的。本文主要研究弱λ-演算的合流变体中的子项分担问题。我们介绍了这个演算的标签，表示一个合流理论的减少与共享，独立的减少策略。我们最后指出，沃兹沃斯的评估技术与共享的子项对应于我们的正式设置。
Despite decades of research in the λ-calculus, the syntactic properties of the weak λ-calculus did not receive great attention. However, this theory is more relevant for the implementation of programming languages than the usual theory of the strong λ-calculus. In fact, the frameworks of weak explicit substitutions, or computational monads, or λ-calculus with a let statement, or super-combinators, were developed for adhoc purposes related to programming language implementation. In this paper, we concentrate on sharing of subterms in a confluent variant of the weak λ-calculus. We introduce a labeling of this calculus that expresses a confluent theory of reductions with sharing, independent of the reduction strategy. We finally state that Wadsworth's evaluation technique with sharing of subterms corresponds to our formal setting.