On interpretation of typed and untyped functional programs

В работе рассматриваются алгоритмы интерпретации типизированных и бестиповых функциональных программ. Типизированные функциональные программы используют переменные любых порядков и константы, порядок которых $\leq 1$, причем константы порядка $1$ являются сильно вычислимыми, монотонными функциями с неопределенными значениями аргументов. Основной семантикой типизированной функциональной программы является функция с неопределенными значениями аргументов, которая является главной компонентой ее наименьшего решения. Алгоритмы интерпретации типизированных функциональных программ основаны на подстановках, $\beta$- редукции и канонической $\delta$-редукции. Основной семантикой бестиповой функциональной программы является бестиповый $\lambda$-терм, полученный посредством использования комбинатора неподвижной точки. Алгоритмы интерпретации бестиповых функциональных программ основаны на подстановках и $\beta$-редукции. Алгоритмы интерпретации исследуются на полноту и сравнимость. Исследуется, также, каким образом меняется “поведение” алгоритмов интерпретации после трансляции типизированной функциональной программы в бестиповую функциональную программу.