On the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms for the canonical notion of $\delta$-reduction

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