ON CANONICAL NOTION OF $\delta$-REDUCTION AND ON TRANSLATION OF TYPED $\lambda$-TERMS INTO UNTYPED $\lambda$-TERMS

Abstract

In the paper typed and untyped $\lambda$-terms are considered. Typed $\lambda$-terms use variables of any order and constants of order $\leq$1. 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.