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’.