A necessary and sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms

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