Лаборатория языковых инструментов

Понятие нормализационного барьера происходит из теории вычислимости, в которой утверждается, что не существует всюду определенной универсальной функция для всех всюду определенных вычислимых функций. Принято считать, что нормализационный барьер означает невозможность написания самоинтерпретатора для строго нормализующего исчисления. В докладе будет подробно рассмотрено строго нормализирующее исчисление F_\omega, показано, почему нормализирующий барьер для него не верен, и представлен его самоинтерпретатор.

Докладчик: Даниил Березун.

Материалы к докладу: Matt Brown and Jens Palsberg. Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega.