On typed and untyped lambda-terms

В работе рассматриваются типизированные $\lambda$-термы, которые используют переменные любых порядков и не используют константы порядка $>1$. Используемые константы порядка $1$ являются сильно вычислимыми функциями, каждая из которых имеет бестиповый $\lambda$-терм, который $\lambda$-определяет ее. Представлен алгоритм трансляции типизированных термов в бестиповые термы, согласно которому каждому типизированному терму $t$ сопоставляется бестиповый терм $t^{\prime}$. Исследуется случай соответствия типизированным термам $t_1\to\to_{\beta\delta}t_2$ бестиповых термов $t_1^{\prime},\, t_2^{\prime}$ таких, что $t_1^{\prime}\to\to_{\beta} t_2^{\prime}$.