On translation of typed functional programs into untyped functional programs

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