用导线减少Lambda项

摘要：

我们引入了一种方法来评估无类型的lambda条款相结合的遍历理论，一个术语树遍历技术的启发游戏语义，明智地使用的eta转换规则的λ演算。简单类型λ演算的遍历理论依赖于eta-long转换，以确保在遍历应用程序时，有一个子项表示每个可能的运算符参数。在无类型设置中，我们通过eta扩展规则的ad-hoc实例化来展示丢失的操作数，这允许遍历继续进行，就像操作数存在于原始项中一样。这就产生了一个更通用的lambda项遍历概念。除了处理无类型的术语之外，一个值得注意的改进是不需要进行初步转换：遍历原始的未更改的lambda术语。我们表明，通过限制自由变量的遍历规则的非确定性，可以有效地计算一组遍历特征的路径在树表示的β-范式，当它存在。这就产生了一个无类型的非线性项的求值算法。我们证明了正确性，遍历实现最左边的线性减少，推广的头部线性减少Danos等。al.

英文摘要：

We introduce a method to evaluate untyped lambda terms by combining the theory of traversals, a term-tree traversing technique inspired from Game Semantics, with judicious use of the eta-conversion rule of the lambda calculus. The traversal theory of the simply-typed lambda calculus relies on the eta-long transform to ensure that when traversing an application, there is a subterm representing every possible operator's argument. In the untyped setting, we instead exhibit the missing operand via ad-hoc instantiation of the eta-expansion rule, which allows the traversal to proceed as if the operand existed in the original term. This gives rise to a more generic concept of traversals for lambda terms. A notable improvement, in addition to handling untyped terms, is that no preliminary transformation is required: the original unaltered lambda term is traversed. We show that by bounding the non-determinism of the traversal rule for free variables, one can effectively compute a set of traversals characterizing the paths in the tree representation of the beta-normal form, when it exists. This yields an evaluation algorithm for untyped lambda-terms. We prove correctness by showing that traversals implement leftmost linear reduction, a generalization of the head linear reduction of Danos et. al.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。