С. Исакова (АУ)

Сложность задачи вывода типов в лямбда-исчислении

Доклад по статье:
Harry G.Mairson "Linear lambda calculus and PTIME-completeness".

В докладе определяются формализмы лямбда-исчисления, просто типизированного
лямбда-исчисления (a la Curry) и рассматривается задача вывода типов в
последнем. Доказывается P-полнота данной задачи при помощи сведения к ней P-полной
задачи о значении булевой схемы на заданном входе. При этом приводится простая
конструкция с использованием стандартных комбинаторов Черча.