Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Веха

Напомню, что HoTT это такая теория типов с филигранным подходом к равенству. Казалось бы, чего можно офилигранить в том, что 1=1?

Мотивация: предположим, у нас есть две абстрактные прямые А и B, обе состоят из континуума плотно линейно упорядоченных точек. Равны ли они?
Они конечно равны однако существует масса неэквивалентных способов идентифицировать на них точки!
Чтобы идентифицировать прямые конкретно, нужно на каждой из прямых выделить по две точки — ноль и единицу, тогда получается что точки каждой из прямых идентифицированны с действительными числами, а стало быть между собой!

Равенство это не «факт», а множество способов идентификации двух объектов.
В HoTT мы пишем A = B и подразумеваем, что множество идентификаций А и B, обозначаемое [A = B] не пусто.

Сами «идентификации», это такие зверьки которые позволяют из фактов про A выводить факты про B. То есть, если для утверждения p про A есть доказательство ev: p(A), то идентификация t: [A = B] даёт нам доказательство t(ev): p(B) такого же утверждения про B.

В том числе, если f(x) = z и t: [x = y], то f(y) = z и в частности f(x) = f(y). Конечно же, использование разных идентификаций из [x = y] даёт разные идентфикации f(x) = f(y).

Примечание 1:
Среди идентификаций двух прямых A и B не существует какой-то выделенной, все их них равноправны. Одну и ту же прямую (скажем, A) тоже можно идентифицировать с собой множеством способов, однако среди них есть выделенный — каждая точка идентифицируется сама с собой. В отличие от классической математики, HoTT понятия «такой же» и «тот же самый» различаются. «Такой же» — это наблюдаемая эквивалентность, максимум что можно сказать о двух данных объектах, не зная их “происхождения”, это что они равны то есть «A такой же как B». Понятие «тот же» это не объективное, а номинальное свойство: A и B ссылаются на один и тот же объект в том и только в том случае, если B было определено через let B := A или соответственно А через let B := A. Для номинальных свойств не выполняется preservation, т.е. подстановка определения вместо определяемого, стирает информацию о тождественности. Данная ситуация совершенно эквивалентна нарушению preservation отношению подтипизации в DOT, что подсказывает возможные пути развития DOT — при необратимых подстановках следует генерировать свидетельство отношения подтипизации и таскать его с собой.

Примечание 2:
Пример с прямыми обобщается на любые алгебраические структуры: с точки зрения HoTT изоморфные реализации алгебраичсккой структуры равны, а изоморфизмы это «способы идентификации». Доказательство этого примечательного факта было опубликовано три дня назад, и это капитальная веха на пути подтверждения состоятельности HoTT.
(http://homotopytypetheory.org/2012/09/23/isomorphism-implies-equality/, не обращайте внимания на идеосинкратическое кодирование модулей, это издержки обозначений.)

Примечание 3:
Объекты (в т.ч. реализации алгебраических структур) равные себе одним единственным образом, называются жёсткими. Равенство между жесткими объектами с одной стороны очень похоже на обычное теоретиком-множественное равенство, а с другой гораздо лучше отражает интуитивно-верную суть вещей, т.к. не делает разницы между разными моделями одной и той же сущности: так например разные модели ряда натуральных чисел (скажем, модель Frege и модель Peano) в теории множеств не равны, тогда как разные минимальные реализации структуры NatObject в HoTT равны. Более того числа 2Frege и 2Peano не равны в теории множеств, не сравнимы (будучи объектами разных типов) в ITT и ETT, и равны в HoTT, что полностью соответствует интуитивному пониманию вопроса.

Платоническую мотивацию я, вроде объяснил, но некоторые программисты, даже очень уважающие философию, всё-таки жаждут конкретных примеров практического применения.

Приложение в математике:
Тип С «набор из N элементов» в обычных типизированных лямбда-исчислениях сконструировать невозможно — у всякого типа данных D должны быть нормальная форма, которая позволяет проверить равенство двух выражений типа D приведением к нормальным формам и сличением. А у «наборов из N элементов» нормальной формы нет — нельзя на компьютере сохранить набор произвольных элементов таким образом, чтобы элементы при этом оставались равноправными, как не извращайся, в процессе сохранения прийдётся расположить элементы в каком-то произвольном порядке.

Что же делать? В HoTT требование канонической нормальной формы смягчается, тут можно изготовить из типа нормальных форм (L = «список из N элементов») и группы симметрий, действующей на нём (тип S = «перестановка списка из N элементов») фактортип M = L/S. Это такой тип который технически состоит в точности из элементов L, однако функции из него f': M => X это только такие функции f: L => X из списков, для которых доказано, что они не зависят от порядка элементов в списке, т.е. s: S => f.s = f. Таким образом получается, что каждый элемент M эквивалентен сам себе |S| разными способами.

Приложение в физике:
В теории поля наблюдаемыми являются поля напряжённостей, конфигурации которых формируют пространство С. Для того, чтобы сформулировать динамику систем в лагранжевом формализме (а это необходимый шаг для квантования, и крайне удобный метод со многих других точек зрения) требуется ввести ненаблюдаемые поля потенциалов, из конфигураций которых c: L существует проекция в конфигурации наблюдаемых полей c': С [платоновых теней реального мира :-)].

Те преобразования L, которые не меняют картины на уровне M называются калибровочными преобразованиями S. Структура калибровочных преобразований S в существенной мере необходима для построения теории, и нужно отметить, что какая-либо информация о ней напрочь отсутствует в пространстве C! Калибровочные преобразования S были «отгаданы» физиками из соображений общей красоты теории.

Формируя M как конструктивный фактортип L/S, мы получаем значительно более богатый объект чем С, т.н. некоммутативное пространство, содержащее все ингридиенты для построения динамической системы.

Возможно на этом пути удастся обрести и понимание других «фантомных» объектов, таких как «поле с одним элементом».

Полученная на этом пути некоммутативная стандартная модель (месяц назад восстановленная в правах перерассчётом массы бозона Хиггса, совместимым с экспериментальными данными) является воплощением заветной мечты Эйнштейна: это общая теория поля, такая что все известные физике поля взаимодействий в ней являются элементами геометрии и их динамика определена простейшим возможным функционалом действия от метрики.

К сожалению, эта теория пока развита только для случая эвклидовой метрики и неизвестно, как бы адаптировать её на случай лоренцевой метрики. Не смотря на то, что локально переход осуществляется просто поворотом Вика, глобально это нетривиальный вопрос, т.к. динамика превращается из элиптической в гиперболическую. Следующим номером нужно будет решить вопрос построения NCSM-термодинамики/статмеханики; в вопросе общерелятевистской термодинамики/статмеханики недавно был совершён прорыв благодаря гипотезе теплового времени, однако обобщение на случай NCSM пока даже не просматривается. Ну и наконец, когда будет понятно, что такое статистическая механика поверх NCSM, можно будет задаться вопросом построения квантовой теории, которая была бы деформацией статистической механики, сводящейся к обычному статмеху в случае характерных макроскопических масштабов. На данный момент вопрос квантования NCSM совершенно непонятен как плане возможной интерпретации (ведь непонятно что такое NCSM-статмех), так и в техническом плане — квантование NCSM очевидно нетривиально по крайней мере в той же мере, что и квантование общей теории относительности, которая десятилетиями считалась абсолютно неприступной (до появления LQG).
Subscribe

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 10 comments

  • (no subject)

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…