On canonical notion of $\delta$-reduction and on translation of typed $\lambda$-terms into untyped $\lambda$-terms

В работе рассматриваются типизированные и бестиповые $\lambda$-термы. Типизированные $\lambda$-термы используют переменные любых порядков и константы порядка $\leq1$, константы порядка $1$ являются сильно вычислимыми функциями с неопределенными значениями аргументов. Каждая функция имеет $\lambda$-определяющий ее бестиповый $\lambda$-терм. Вводится так называемое каноническое понятие $\delta$-редукции, которая используется при реализации функциональных языков программирования. Для канонического понятия $\delta$-редукции исследуется трансляция типизированных $\lambda$-термов в бестиповые $\lambda$-термы.