Reducing Lambda Terms with Traversals

TL;DR

This paper presents a novel traversal-based method for evaluating untyped lambda calculus terms by integrating eta-expansion, enabling direct traversal of original terms without prior transformation, and proving its correctness.

Contribution

It introduces a generic traversal approach for untyped lambda terms using eta-expansion, eliminating the need for term transformation prior to evaluation.

Findings

Effective computation of traversals characterizing beta-normal form paths.

Traversal method implements leftmost linear reduction.

No preliminary transformation needed for original lambda terms.

Abstract

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.