On main canonical notion of $\delta$-reduction

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