UNTYPED LAMBDA-CALCULUS NORMALIZATION BY TRAVERSALS
Normalization by traversals is a new approach to normalization of lambda-terms by tracing their abstract syntax trees. Originally designed is context of simply-typed lambda-calculus, it was then extended to untyped lambda-calculus but this extension has no formal presentation and correctness proof. In the paper we present the first formal presentation of untyped lambda-calculus normalization by traversals procedure via transition system and show its correctness with respect to the linear reduction.