На смерть Воеводского

[george66]

Попытаюсь объяснить, чем занимался Воеводский последние годы. Сначала предыстория. Обозначим $List(n)$ множество (лучше будем говорить "тип") всех конечных списков действительных чисел длины $n$. Напишем такое утверждение ("секвенцию")
$n:\mathbb{N}\vdash List(n):Type$
"если $n\in\mathbb{N}$, то $List(n)$ является правильно построенным типом".
Поскольку $4\in\mathbb{N}$, мы можем заключить $List(4):Type$. Элементами типа $List(4)$ будут списки длины 4, например
$(1.0,1.0,1.0,0.0): List(4)$
Далее $2\times 2\in\mathbb{N}$, поэтому $List(2\times 2):Type$
Поскольку $2\times 2=4$, хочется написать
$List (2\times 2)=List(4)$
и считать, что любой элемент типа $List(2\times 2)$ является также элементом типа $List(4)$ и наоборот. В данном случае это не создаёт проблем, потому что равенство $List (2\times 2)=List(4)$ легко проверяется. Но в общем случае, если параметр не натуральное число, а, допустим, действительное число или какая-нибудь сложная фигня, проверка равенства может стать сколь угодно сложной.
Пусть дан некоторый тип $A:Type$. Пусть также дан тип, зависящий от параметра
$x: A\vdash B(x):Type$
Пусть даны два элемента типа $A$
$a_1\in A$
$a_2\in A$
Пусть мы доказали (мучительно трудно), что они равны $a_1=a_2$. Следует ли из этого, что $B(a_1)=B(a_2)$ и любой элемент типа $B(a_1)$ является также элементом типа $B(a_2)$ ? Напишем выражение $\lambda x\!:\! B(a_1).\,x$ обозначающее тождественную функцию из $B(a_1)$ в $B(a_1)$, эта функция принадлежит типу $B(a_1)\to B(a_1)$ всех функций из $B(a_1)$ в $B(a_1)$
$\lambda x\!:\! B(a_1).\,x: B(a_1)\to B(a_1)$
Можем ли мы сказать, что то же самое выражение $\lambda x\!:\! B(a_1).\,x$ принадлежит типу $B(a_2)\to B(a_2)$, поскольку $B(a_1)=B(a_2)$ ?
$\lambda x\!:\! B(a_1).\,x: B(a_2)\to B(a_2)$
Это кажется неприятным. Раньше мы легко могли проверить правильность утверждений вида $t: T$ ("что-то является элементом чего-то"), теперь же нам для этого придётся проверять равенство $a_1=a_2$, что может быть очень сложным делом. Поэтому возобладала мысль, что равенство типов -- это не точное совпадение, а только изоморфизм. Допустим, у нас есть доказательство $p$ равенства $a_1=a_2$, что мы запишем так
$p: a_1=a_2$
равенство теперь само становится типом, элементами которого являются "конструкции, подтверждающие равенство $a_1$ и $a_2$" или "доказательства равенства $a_1$ и $a_2$". По этому $p$ мы можем построить изоморфизм типов $B(a_1)$ и $B(a_2)$, который можно обозначить $B(p)$
$B(p): B(a_1)\to B(a_2)$
(кто знаком с теорией категорий, тут вспомнит слово "функтор". Тип, зависящий от параметра, становится некоторым функтором). Далее, можно построить изоморфизм между типами $B(a_1)^{ B(a_1)}$ и $B(a_2)^ {B(a_2)}$ (пожалуй, обозначу его $B^B(p)$) и добиваться, чтобы выражение
$B^B(p)(\lambda x\!:\! B(a_1).\,x)$ вычислялось (редуцировалось) к $\lambda x\!:\! B(a_2).\,x$
Всё это восходит к Мартин-Лёфу, далее разные люди создавали громоздкие исчисления, мало кому интересные за пределами теоретико-типовой тусовки. Продолжение следует.

-- 01.10.2017, 23:10 --

Точнее сказать, всё это пытались применять к компьютерной проверке доказательств. Существуют формальные языки, позволяющие строго записывать математические доказательства (с той же строгостью, с какой мы записываем алгоритмы на языках программирования). Длина формально записанного доказательства обычно раз в двадцать-тридцать больше длины обычного, какое мы посылаем в математический журнал. Зато правильность формального доказательства можно проверять автоматически с помощью простой программы-проверяльщика, которая называется "пруфчекер". И вот Воеводский увлёкся таким делом: строго записывал свои доказательства (про гомотопии) и проверял пруфчекером. И ему пришла идея, что этот "тип равенства" можно понимать с точки зрения гомотопий. Возьмём некоторую поверхность $A$, будем считать её типом. Возьмём две её точки $a_1,a_2$ это элементы типа $A$. Пусть $p$ путь, соединяющий $a_1$ и $a_2$, будем считать его элементом соответствующего типа равенства $a_1=a_2$ и писать
$p:a_1=a_2$
Таким образом, точки считаются равными, если их можно соединить путём. Пусть даны два пути из $a_1$ в $a_2$
$p_1:a_1=a_2$
$p_2:a_1=a_2$
Мы можем и для них выписать тип равенства $p_1=p_2$, его элементами будут гомотопии путей
$\alpha:p_1=p_2$
Два пути считаются равными, если они гомотопны. Можно рассматривать и равенство гомотопий, элементами соответствующего типа будут "непрерывные деформации гомотопий друг в друга". Таким образом, язык теории типов с типом равенства, по Воеводскому, очень хорошо подходит, чтобы говорить о гомотопиях (а также формализовать соответствующие доказательства и проверять пруфчекером). Продолжение следует.

-- 01.10.2017, 23:15 --

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

[arseniiv]

Ну с равенством-то ситуация немного интереснее. Вот вы упомянули Мартин-Лёфа, а наверно стоило с него и начать. Он рассмотрел теории типов с интенсиональным и экстенсиональным равенством, и т. д.. А так как-то скомкано, не поймут ещё.

[kp9r4d]

Так, но всё же интерес HoTT не только в том, что основания, а ещё и в том, что если гомотопические группы сфер посчитать так и эдак то выйдет одно и то же, да?

[arseniiv]

Может быть, это описано в The HoTT Book, гляньте, если ещё нет — тип сфер там точно рассматривался, и раздел о собственно гомотопиях и всяких топологических штуках там есть, но я его почти не читал и всё равно вряд ли бы понял, не зная введения в них.

Кстати, где-то не очень давно писали, что, вроде бы, ещё так и не показали, что у HoTT действительно такие модели, что можно говорить о гомотопиях и прочих вещах. (Скорее всего, я испорченный телефон.) А вот что это внутренний язык каких-то $n$-категорий, вроде, известно точно.

[kp9r4d]

Да от меня наверное и слышали, я сюда вбрасывал когда-то инфу про syntax semantics duality, что это внутренний язык для элементарного $(\infty,1)$-топоса, летом очень увлекался HoTT и таким всем, но теперь учебный год начался и теперь нужно увлекаться стабильными $(\infty,1)$-категориями, что тоже неплохо. И там довольно мутноватая история про сферы и про то, что вообще можно, а что нельзя считать вменяемым доказательством гомотопических гипотез. Думал george66 что-то об этом скажет дополнительно.

[george66]

Гомотопные математики давно (с Гротендика) пытаются формализовать "категории высшего порядка". Это такие категории, где между объектами стрелки, между стрелками "стрелки второго порядка", между ними "стрелки третьего порядка" и т.д. Даны определения категорий второго порядка, третьего (тяжёлое) и четвёртого (совершенно адское), которое все специалисты признают "правильными". Начиная с пятого есть несколько адских определений, про которые неизвестно, равносильны ли они между собой. Когда мы изучаем тип равенства, нам нужен более узкий класс категорий. Каждый тип воспринимается как категория, его элементы как объекты, а доказательства равенства $p:a_1=a_2$ будут стрелками, причём все стрелки - изоморфизмы (такие категории называются "группоидами"). Дальше мы хотим рассматривать гомотопии $\alpha:p_1=p_2$ в качестве "стрелок второго порядка" и так далее, получаем "группоиды высшего порядка", которые пытался определить Гротендик.

[george66]

Вот сам Воеводский рассказывает, как он пришёл к необходимости компьютерной проверки доказательств и новым основаниям (интересный момент - в его старой статье нашлась ошибка через 22 года после публикации)

https://www.math.ias.edu/vladimir/sites ... 14_IAS.pdf

[george66]

Вот, кто хочет оценить, определение 4-категории (существует только в таком виде)

http://math.ucr.edu/home/baez/trimble/t ... ories.html

Хотите ли вы таких оснований?

[kp9r4d]

Так, ну в коде таких ужасов нету, а inf-группы есть, что наводит на мысли, что можно и без точных дефинишинов 4-категорий жить.

[george66]

ZF как раз хороша тем, что можно обойтись без неё. Реально можно формализовать свой кусочек математики без всякой ZF. Тут нам предлагают такие основания, от которых уже не убежишь. Даже если удастся дать работающие определения n-категорий и выписать соответствующие теории типов, зачем ставить на такую опору всю математику? Я не хочу это изучать, я изучал, мне не понравилось. Пока что единственный приятный подход к n-категориям -- это пруфчекер Globular, где вместо формул рисуют картинки (string diagrams) и доказательства строят в графическом редакторе в виде набора картинок. Придумали его, что характерно, люди со стороны (квантовые физики) с незамыленным взглядом.

https://golem.ph.utexas.edu/category/20 ... bular.html

[kp9r4d]

Ну потому что вся самая высокоуровневая математика и физика без $\infty$-категорий не обходится, и интуитивно кажется, если стартовать с них, то высокоуровневые результаты в пруфчерек загонять будет проще, а другие неинтересны.

[arseniiv]

Мне вот теории, включающие λ-исчисление, кажутся чуть более удобными для выражения вещей. Есть у кого-нибудь λ-теория множеств?

[GOLOTOPAXPOP]

kp9r4d в сообщении #1253170 писал(а):

Ну потому что вся самая высокоуровневая математика и физика без $\infty$-категорий не обходится, и интуитивно кажется, если стартовать с них, то высокоуровневые результаты в пруфчерек загонять будет проще, а другие неинтересны.

Если частенько читать ncatlab, и при этом принимать все за чистую монету, и такое впечатление может сложиться. Не будет это сказано в обиду. На тот сайт пишет много различных людей с различными бэкграундами, но костяк старожил - это все-таки по темпераменту математические логики, что само по себе ничуть не плохо, пока человек не пытается "все взять и переопределить" для остальных математиков. Ну и то, что они сами себя заявляют, как "math, physics and philosophy", как бы намекает. Философия - это, опять таки, прекрасно, но надо отдавать себе отчет, что занимаешься вещами, интересными с философской точки зрения, но не факт, что с математической (не зря в US и UK (математические) логики и математики на отдельных департаментах сидят), с чем у некоторых (не всех ни в коем случае) людей с ncatlab'а проблемы.

Давайте будем честны, не "физика", а "математическая физика", и не "вся", а отдельные работы отдельных людей (Urs Schreiber, например, Lurie и ко. с cobordism hypothesis и классификацией TQFT). То есть это даже не 0,05 процентов от всей математической физики.

Что касается математики, то ещё большая неправда. Но вы, судя по этому форуму, интересуетесь различными вещами - в том числе и классическим анализом, где никакие категории и не валялись, а не только абстрактно-категорной математикой, так что я думаю, вы и сами это понимаете.

[george66]

Более-менее соответствует теории множеств исчисление HOL (High Order Logic), на котором основан пруфчекер Isabelle. Там теория типов с экспонентой (типовое лямбда-исчисление), причём есть тип $\Omega$, у элементов которого (формул) есть свои элементы (доказательства, это подвальный этаж). В пруфчекере Coq, которым пользовался Воеводский, множества и формулы не различаются, каждый тип можно считать и множеством и формулой.

-- 05.10.2017, 00:28 --

GOLOTOPAXPOP в сообщении #1253181 писал(а):

kp9r4d в сообщении #1253170 писал(а):

Ну потому что вся самая высокоуровневая математика и физика без $\infty$-категорий не обходится, и интуитивно кажется, если стартовать с них, то высокоуровневые результаты в пруфчерек загонять будет проще, а другие неинтересны.

Если частенько читать ncatlab, и при этом принимать все за чистую монету, и такое впечатление может сложиться. Не будет это сказано в обиду. На тот сайт пишет много различных людей с различными бэкграундами, но костяк старожил - это все-таки по темпераменту математические логики, что само по себе ничуть не плохо, пока человек не пытается "все взять и переопределить" для остальных математиков.

Не надо гнать на математических логиков, я математический логик и гомотопий не люблю. Даже написал учебник теории категорий без гомотопий.

[GOLOTOPAXPOP]

george66 в сообщении #1253038 писал(а):

Вот, кто хочет оценить, определение 4-категории (существует только в таком виде)

http://math.ucr.edu/home/baez/trimble/t ... ories.html

Хотите ли вы таких оснований?

Не специалист (я), но разве обычные $n$-категории имеют особое отношение к "ядру" HoTT? Там же, вроде, вся теория базируется на $\infty$-группоидах, и так далее? А на Воеводского ещё оставил отпечаток его опыт с Блохом-Като, где алгебраическая геометрия, но ни каких $n$-категорий (хотя теория базируется на теории модельных категорий, которые связаны с $(\infty,1)$, но и $(\infty,1)$ никакого отношения к $n$-категориям в целом не имеет: там, скорее, людей интересуют $(\infty,n)$ и $\omega$ (то есть $(\infty,\infty)$ категории).

HoTT же, точнее, шум вокруг неё, конечно, мутная вещь. Как раздел логики она прекрасна, но вот все эти помпезные разговоры про переписывание ВСЕЙ математики на её язык, так сказать, не комильфо.