ON TYPED AND UNTYPED LAMBDA-TERMS - Khondkaryan, T.V. (Proceedings of the YSU A: Physical and Mathematical Sciences, 2015)
Typed $λ$-terms that use variables of any order and don't use constants of order $>1$ are studied in the paper. An algorithm of translation of typed $λ$-terms to untyped $λ$-terms is presented. According to that algorithm, each typed term $t$ is mapped to an untyped term $t'$. We study in which case typed terms $t_1$, $t_2$ such that $t_1 → →_{βδ} t_2$ correspond to untyped terms ${t_1}',{t_2}'$ such that ${t_1}' →→_β {t_2}'.$
Keywords: typed $λ$-terms, untyped $λ$-terms, translation, $β$-reduction, $δ$-reduction