Evaluating Lambda Terms with Traversals

A method to evaluate untyped lambda terms based on a term tree-traversing technique inspired by Game Semantics and judicious use of eta-expansion. As traversals explore nodes of the term tree, they dynamically eta-expand some of the subterms in order to locate their non-immediate arguments. A quantity called dynamic arity determines the necessary amount of eta-expansion to perform at a given point. Traversals are finitely enumerable and characterize the paths in the tree representation of the beta-normal form when it exists. Correctness of the evaluation method follows from the fact that traversals implement leftmost linear reduction, a non-standard reduction strategy based on head linear reduction of Danos-Regnier.