A self-interpreter of lambda calculus having a normal form

We formalize a technique introduced by B\"{o}hm and Piperno to solve systems of recursive equations in lambda calculus without the use of the fixed point combinator and using only normal forms. To this aim we introduce the notion of a canonical algebraic term rewriting system, and we show that any such system can be interpreted in the lambda calculus by the B\"{o}hm - Piperno technique in such a way that strong normalization is preserved. This allows us to improve some recent results of Mogensen concerning efficient g\"{o}delizations $\godel{~}: \Lambda \rightarrow \Lambda$ of lambda calculus. In particular we prove that under a suitable g\"{o}delization there exist two lambda terms $\bf E$ (self-interpreter) and $\bf R$ (reductor), both having a normal form, such that for every (closed or open) lambda term $M\;$ ${\bf E}\godel{M} \reduce M$ and if $M$ has a normal form $N$, then ${\bf R}\godel{M} \reduce \godel{N}$