По просьбе os80 пишу ещё раз об унивалентности в ЖЖ

[akuklev]

(P.S. Кажется, я научился быстро писать. Весь нижеследующий пост написался за 15 минут за едой.)

Гомотопическая теория типов HoTT это такой фреймворк для деланья математики и одновременно язык программирования. Среди довольно обширного семейства таких систем* HoTT примечательна тем, что gets equality right.

Comments

[ex_juan_gan]

О, спасибо!

Между тем, Z specification language, на который аж есть ISO стандарт, очень мило перемешивает типы и множества, просто чуть не в коде иллюстрируя эти проблемы.

[alla_maria]

по сабжу ничего сказать не могу, но приятно увидеть, что ты подаешь признаки жизни;)

[akuklev]

Да ну просто дел много. :-)

[os80]

Прежде всего, громадное спасибо за отклик на чаяния масс в виде меня :-) У меня было нехорошее подозрение, что я (попытавшись читать HoTTBook) просто неправильно что-то переводил. Проблема, однако, более глубокая (я не понимаю кое-что на сущностном уровне), поэтому разрешите задать пару вопросов.
типы a = b теперь интерпретируются не как тип доказательств равенства a и b, а как тип сохраняющих структуру обратимых переходов от a к b
1. Что такое а и b? Может быть такое, что, например, а это число 3, а b - это число 6? Или, скажем, это больше похоже на "пусть a это множетство целых чисел, а b - множество чётных чисел"? Или даже на "пусть a это кольцо целых чисел, а b - кольцо чётных чисел"?
2. Что такое "обратимый переход"? Биекция/изоморфизм?
3. Что такое "3=6"? "Множество/класс" преобразований, переводящих 3 в 6? "Множество/класс" таких обратимых преобразований?
4. Что такое "Z = (Z/2Z)"? Умножение на двойку? Умножение на двойку в композиции со всеми перестановками?

[thedeemon]

a и b могут быть числами, функциями, типами, чем угодно, лишь бы одного типа.
Рассматривая их тип как пространство, а их самих как точки, значение "a=b" это путь в таком пространстве, а тип "a=b" это просто тип. В случае 3 и 6 такой тип будет ненаселен - не будет значений такого типа, нет пути из 3 в 6. Ибо натуральный числа - это дискретное пространство, там все пути идут из точки в саму себя, разные точки не соединяются.

В случае когда a и b это типы (вроде того же Z), уже интереснее. Там могут быть нетривиальные пути, и пространство этих путей эквивалентно пространству изоморфизмов между ними, что унивалентность и постулирует.

[os80]

>там все пути идут из точки в саму себя, разные точки не соединяются.
Почему? Что такое вообще "путь". akuklev перевёл path как "обратимый переход, сохраняющий структуру". Не знаю, насколько это верно, но хотя бы приблизительно понятно. Вы же используете понятие "пути" в каком-то нестандартном смысле и не вводите это понятие.

[akuklev]

Можно вместо "обратимый переход" попробовать термин "соответствие". Вот элемент множества неупорядоченных пар соответствует самому себе двумя способами: прямо так и с отзеркаливанием. Эти два способа совпадают между собой только если оба элемента пары равны.

[migmit]

Что-то у меня с этим ба-альшие проблемы. Попробую сформулировать

[akuklev]

Тут немного другая аналогия уместней: математики пишут псевдокод, и подразумевают что он как-то компилируется в ассемблер (теорию множеств). Можно заменить ассемблер хасекелем (т.е. теорию множеств на HoTT), математики все так же будут писать псевдокод, но подразумевать что он компилируется в Хаскель. Дистанция от пседокода до ассемблера так велика, что (а) на практике перевод ужасающе сложен и (б) из ассемблерного кода без комментариев вообще не видно, что хотел сказать автор. Дистанция от псевдокода до хаскеля значительно меньше.

Что не отменяет низкоуровневости. Агда конечно в разы ближе к ассемблеру, чем к псевдокоду, на котором пишутся серьёзные доказательства нетривиальных теорем.

[migmit]

Да, это, в общем-то, то, что я имел в виду.

И когда я вижу, как люди говорят, что "современное математическое доказательство невозможно перевести в понятия теории множеств", мне всё время кажется, что меня убеждают, что ни Microsoft Word-а, ни, тем более, GHC, не существует и существовать не может.

Пардон, это была личная болячка.

[anonymous]

а что за обратная математика и кто такой феферман?
википедия отказывается дружить со мной по этому поводу :(

[akuklev]

http://en.wikipedia.org/wiki/Reverse_mathematics
http://en.wikipedia.org/wiki/Solomon_Feferman