MIPT-Coq-24-Lect-02

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: теорема Чёрча--Россера, вопросы существования и единственности нормальной формы; представление булевых функций комбинаторами, композиция сохраняет представимость; условный переход и кодирование пар; нумералы Чёрча представление арифметических функций и предикатов; итерация: функция "предшественник", примитивная рекурсия сохраняет представимость; комбинатор неподвижной точки, явная рекурсия, совместная рекурсия.