Попытаюсь объяснить, чем занимался Воеводский последние годы. Сначала предыстория. Обозначим
множество (лучше будем говорить "тип") всех конечных списков действительных чисел длины
. Напишем такое утверждение ("секвенцию")
"если
, то
является правильно построенным типом".
Поскольку
, мы можем заключить
. Элементами типа
будут списки длины 4, например
Далее
, поэтому
Поскольку
, хочется написать
и считать, что любой элемент типа
является также элементом типа
и наоборот. В данном случае это не создаёт проблем, потому что равенство
легко проверяется. Но в общем случае, если параметр не натуральное число, а, допустим, действительное число или какая-нибудь сложная фигня, проверка равенства может стать сколь угодно сложной.
Пусть дан некоторый тип
. Пусть также дан тип, зависящий от параметра
Пусть даны два элемента типа
Пусть мы доказали (мучительно трудно), что они равны
. Следует ли из этого, что
и любой элемент типа
является также элементом типа
? Напишем выражение
обозначающее тождественную функцию из
в
, эта функция принадлежит типу
всех функций из
в
Можем ли мы сказать, что то же самое выражение
принадлежит типу
, поскольку
?
Это кажется неприятным. Раньше мы легко могли проверить правильность утверждений вида
("что-то является элементом чего-то"), теперь же нам для этого придётся проверять равенство
, что может быть очень сложным делом. Поэтому возобладала мысль, что равенство типов -- это не точное совпадение, а только изоморфизм. Допустим, у нас есть доказательство
равенства
, что мы запишем так
равенство теперь само становится типом, элементами которого являются "конструкции, подтверждающие равенство
и
" или "доказательства равенства
и
". По этому
мы можем построить изоморфизм типов
и
, который можно обозначить
(кто знаком с теорией категорий, тут вспомнит слово "функтор". Тип, зависящий от параметра, становится некоторым функтором). Далее, можно построить изоморфизм между типами
и
(пожалуй, обозначу его
) и добиваться, чтобы выражение
вычислялось (редуцировалось) к
Всё это восходит к Мартин-Лёфу, далее разные люди создавали громоздкие исчисления, мало кому интересные за пределами теоретико-типовой тусовки. Продолжение следует.
-- 01.10.2017, 23:10 --Точнее сказать, всё это пытались применять к компьютерной проверке доказательств. Существуют формальные языки, позволяющие строго записывать математические доказательства (с той же строгостью, с какой мы записываем алгоритмы на языках программирования). Длина формально записанного доказательства обычно раз в двадцать-тридцать больше длины обычного, какое мы посылаем в математический журнал. Зато правильность формального доказательства можно проверять автоматически с помощью простой программы-проверяльщика, которая называется "пруфчекер". И вот Воеводский увлёкся таким делом: строго записывал свои доказательства (про гомотопии) и проверял пруфчекером. И ему пришла идея, что этот "тип равенства" можно понимать с точки зрения гомотопий. Возьмём некоторую поверхность
, будем считать её типом. Возьмём две её точки
это элементы типа
. Пусть
путь, соединяющий
и
, будем считать его элементом соответствующего типа равенства
и писать
Таким образом, точки считаются равными, если их можно соединить путём. Пусть даны два пути из
в
Мы можем и для них выписать тип равенства
, его элементами будут гомотопии путей
Два пути считаются равными, если они гомотопны. Можно рассматривать и равенство гомотопий, элементами соответствующего типа будут "непрерывные деформации гомотопий друг в друга". Таким образом, язык теории типов с типом равенства, по Воеводскому, очень хорошо подходит, чтобы говорить о гомотопиях (а также формализовать соответствующие доказательства и проверять пруфчекером). Продолжение следует.
-- 01.10.2017, 23:15 --Далее история, на мой сильно пристрастный взгляд, перестаёт быть приличной. На форуме теории типов много лет стоял печальный стон "Почему программистам не интересно то, что мы делаем?" Программистов они воспринимали как главную целевую аудиторию. Тут пришёл Воеводский, большой авторитет, Филдсовский лауреат и принёс идею. Возник удивительный для меня энтузиазм "Нафиг программистов, давайте охмурять гомотопных математиков! Спихнём теорию множеств, всё будет нашим!" Вся голодная орда бросилась изучать гомотопии. Представьте, что лямбда-исчисление каким-то образом оказалось бы приложимо к интегралу Фурье и все специалисты по языку Хаскел бросились изучать интеграл Фурье с криками "Наконец то мы нашли смысл жизни!" Вот именно это и случилось. Воеводский, надо сказать, быстро отошёл в сторону, не будучи специалистом в этой области, но его уже не надо было. Сорок человек вместе написали книжку (HoTT). Дальше больше, в своих документах они это называют "основания математики 21-го века". И тут Воеводский, с присущей ему оригинальностью, взял да и умер. Предсказываю, что HoTT теперь съёжится до умеренных размеров, а все основатели математики 21-го века уберутся туда, откуда родились.