Напомню, что 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 равны. Более того числа 2
Frege и 2
Peano не равны в теории множеств, не сравнимы (будучи объектами разных типов) в 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| разными способами.
Приложение в физике:( Read more... )