Тема нынче довольно модная и распиаренная. Денис рассказывал, что даже программисты у него на работе обсуждали эту деятельность, несмотря на ее абсолютно теоретический характер. В МГУ на топологических семинарах это тоже обсуждалось. Мое любопытство тоже затронуло, и года три назад я решил немного взботнуть книгу https://homotopytypetheory.org/book/ (она вроде пока единственная, поскольку там в авторах - все, кто вообще этой темой серьезно занимается). В книге хотели угодить всем: и топологам, и логиками, и программистам, поэтому лично мне, как не логику, и не программисту, тяжело было читать. Да я и не дочитал, собсно.
Недавно понял, что всю эту деятельность можно охарактеризовать несколько дзенской фразой:
"Доказательство есть путь"
Только вот гомотопические типовики ее понимают вполне буквально. Подробнее...
Логика
В математике есть утверждения и есть доказательства. С одной стороны, доказательства - это некие морфизмы между утверждениями, т.е. процедуры, позволяющие переходить от утверждения А к утверждению Б. С другой стороны, каждое доказательство - это тоже некое утверждение, т.е. объект (тут наблюдается связь с темой предыдущей заметки). А значит, у нас существуют
объекты (утверждения),
морфизмы между объектами (доказательства утверждений),
морфизмы между морфизмами (доказательства эквивалентности доказательств) - это называется 2-морфизмами,
морфизмы между 2-морфизмами (доказательства эквивалентности доказательств эквивалентности доказательств) - это 3-морфизмы,
и т.д.
Такая структура называется ∞-категорией. В теории типов (без эпитета "гомотопический" эта теория существует уже давно) не хотят различать все эти n-морфизмы. Вместо этого вводится понятие типа. В простом понимании, тип - это утверждение. Типу-утверждению можно сопоставить множество всех его доказательств, поэтому до некоторой поры типы можно понимать как множества.
Пустой тип - это ложное утверждение, т.е. утверждение, для которого нет ни одного доказательства. Конструктивизм тут как тут: нет доказательств => утверждение неверно.
Имея некий запас типов, можно строить новые типы по формальным правилам, как это делается в проге. Например, имея типы А и Б, можно построить тип (А->Б) - он означает утверждение, что из А следует Б. Если тип (А->Б) пустой, это попросту означает, что из А не следует Б. Но если же тип (А->Б) не пустой, то это не просто означает, что из А следует Б. Тип (А->Б) как бы содержит в себе все возможные способы вывести из утверждения А утверждение Б, а это гораздо более богатая структура. Например, для двух элементов C, D типа (А->Б) мы можем поинтересоваться, эквивалентны ли они, т.е. является ли тип (C=D) непустым.
*конечно, нужно строго определить, что такое элемент C типа Х и указать конструктор для типа (C=D), чтобы вся эта хрень вообще имела смысл. Это долго и занудно делается в упомянутой выше книге. Более того, говорят не "С является элементом типа Х", а просто "С имеет тип Х", как в проге.
Короче говоря, мы смотрим не только на истинность/ложность утверждения, но и на структуру всех возможных доказательств утверждения.
Топология
Нечто подобное возникает в топологии. Работая с топологическим пространством, мы можем рассмотреть ∞-категорию, в которой:
объекты - точки пространства;
морфизмы - пути между точками;
2-морфизмы - пути между путями (т.е. гомотопии путей);
3-морфизмы - пути между путями между путями (т.е. гомотопии двумерных клеток);
и т.д.
Всю важную гомотопическую информацию о пространстве эта структура сохраняет. Из нее понятным образом извлекается число компонент связности, фундаментальная группа, старшие гомотопические группы и прочая.
Микс
Аналогия топологии с логикой налицо. Так и возникает гомотопическая теория типов. Теперь можно понимать каждый тип А как топологическое пространство: доказательства утверждения А - это точки пространства, доказательства эквивалентности доказательств - это пути между точками и т.д.
(*можно строить топологию не через системы открытых множеств, а через категорную алгебру - гомотописты это особенно любят. здесь под топологическим пространством понимается как раз такая абстрактная шняга)
Дальнейшие фокусы вообще разрывают мозг. Существует тип "Тип". По сути это утверждение о том, что нечто является типом. Т.е. А имеет тип "Тип" <=> А - это тип. Внезапно, да? Тип "Тип" - это некая замена для несуществующего в обычной логике множества всех множеств. Поскольку тип "Тип" - это тоже тип, он тоже "имеет структуру топологического пространства". Получается, что вся логика, т.е. совокупность всех утверждений, - это некое страшное топологическое пространство.
(Отвлечение в сторону. Есть одна известная, но непонятная мне идея. Утверждается, что категория всех топологических пространств сама похожа на топологическое пространство в некотором смысле. Это воодушевляет, хоть и таинственно.)
Аксиома унивалентности.
Имея два типа А и Б, можно сконструировать тип (А=Б), обозначающий их тождественное равенство. А можно еще сконструировать тип (А~Б), кодирующий утверждение о гомотопической эквивалентности топологических пространств А и Б. Аксиома унивалентности постулирует что
((А=Б)~(А~Б))
т.е. что такой тип непуст. Иными словами, постулируется, что тождественное равенство и гомотопическую эквивалентность в теории можно не различать... с точностью до гомотопической эквивалентности.
Эта аксиома мне кажется весьма забавной. Например, можно взять два типа-утверждения: "единорогов не существует" и "дважды два - четыре". Если они обладают одной и той же структурой доказательств, скажем, и там и там возникает ∞-категория окружности, то можно считать, что эти утверждения тождественны. Безотносительно их реального смысла. Круто же! Хотя и неудивительно.
Пошто?
Интерес к гомотопической теории типов подогревается тем, что ее адепты обещают явить миру абстрактную систему компьютерной проверки математических доказательств. Надо думать, что проверять она будет только категорно-тополого-алгебраические доказательства, т.е. те, чья структура так или иначе зашита в саму теорию. Тут похоже на квантовые компы. Как рассказывал Игорь Молчанов в лмш, - в Doom на квантовом компе не поиграешь, но рассчеты из самой квантовой физики на системе с похожим принципом работы производить должно быть естественно (если их когда-нибудь вообще доведут до ума). Гомотопическая теория типов - это из той же серии: сомнительно, что для проверки каких-то далеких от топологии утверждений нужна вся эта символьно-гомотопическая йога.
Комментариев нет:
Отправить комментарий