On canonical notion of $\delta$-reduction and on translation of typed $\lambda$-terms into untyped $\lambda$-terms

In the paper typed and untyped $\lambda$-terms are considered. Typed $\lambda$-terms use variables of any order and constants of order $\leq1$. Constants of order $1$ are strong computable functions with indeterminate values of arguments and every function has an untyped $\lambda$-term that $\lambda$-defines it. The so-called canonical notion of $\delta$-reduction is introduced. This is the notion of $\delta$-reduction that is used in the implementation of functional programming languages. For the canonical notion of $\delta$-reduction the translation of typed $\lambda$-terms into untyped $\lambda$-terms is studied.