(no subject)

[66george]

Первая попытка писать на Lean4 (пустые строки убрал, чтобы всё поместилось). Перевод обычных лямбда-термов в де Брёйновские. Решил закончить пару висяков. Некоторое время назад придумал новое определение альфа-конверсии (новый способ определять ту же самую альфа-конверсию), который мне кажется гораздо лучше прежних, что подтвердил и Куклев. Доказать соответствие обычных и де Брёйновских термов не просто трудно, а совершенно адски трудно (поэтому обычно вопрос замалчивают). Надо доказать, что подстановка на обычных термах соответствует подстановке на де Брёйновских, притом определяются они совершенно по-разному и, главное, обычные термы надо рассматривать с точностью до альфа-конверсии, которая сама определяется через подстановку (при обычном подходе, у меня без неё). Если энтузиазм не пропадёт и всё проверю пруфчекером, немедля вставлю в новую книгу первой главой (и назову "Что скрывал Барендрегт", шутка). Взялся обдуманно, просмотрел руководства по Isabelle, Coq и Lean. Руководство Lean явно лучше написано. Поставил последнюю версию Lean (Lean4) и обнаружил, что руководство написано для предпоследней, причём обратной совместимости нет (и примеры из учебника не работают). И вот так у них всё! Для последней же версии учебник только начали писать, приходится всё спрашивать на форуме.