In this short paper we develop a function in lambda calculus which normalizes another lambda term given as an argument. I.e. we simulate computation of lambda calculus (i.e. beta reduction) within lambda calculus.
The normalizing function needs only one partial function to do the job. All other used functions are total. The same key idea is used when proving that all computable functions have a \emph{Kleene Normal Form}.
In this paper a programming notation for lambda calculus is used in order to make the subject accessible for programmers and not only for mathematicians.
pdf