ON CANONICAL NOTION OF $δ$-REDUCTION AND ON TRANSLATION OF TYPED $λ$-TERMS INTO UNTYPED $λ$-TERMS - Nigiyan, S.A.; Khondkaryan, T.V. (Proceedings of the YSU A: Physical and Mathematical Sciences, 2017)
In the paper typed and untyped $λ$-terms are considered. Typed $λ$-terms use variables of any order and constants of order $≤$1. Constants of order 1 are strong computable functions with indeterminate values of arguments and every function has an untyped $λ$-term that $λ$-defines it. The so-called canonical notion of $δ$-reduction is introduced. This is the notion of $δ$-reduction that is used in the implementation of functional programming languages. For the canonical notion of $δ$-reduction the translation of typed $λ$-terms into untyped $λ$-terms is studied.
Keywords: typed $λ$--term, untyped $λ$-term, translation, notion of $δ$-reduction, $λ$-definability