  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.
