@misc{blum2018reducing,
author = {Blum, William},
title = {Reducing Lambda Terms with Traversals (preprint)},
year = {2018},
month = {February},
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.},
url = {http://approjects.co.za/?big=en-us/research/publication/reducing-lambda-terms-with-traversals-preprint/},
note = {Preprint},
}