![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Jul. 3rd, 2012
Допустим у нас есть несколько ценных теорем о функции f, использующей в теле stableSort1. Теперь допустим у нас есть функция stableSort2, которая работает как stableSort1 в том смысле, что на одинаковых input'ах даёт одинаковые output'ы, и у нас есть доказательство этого факта. В OTT это позволяет всегда сделать вывод, что все теоремы об f верны также и для функции f', которая отличается от f только тем, что в ряде мест stableSort1 заменили на stableSort2.
А HoTT нужен на случай unstableSort'ов. Если у нас есть две не обязательно стабильных функции сортировки w и v: {A : Set} -> {{O : PartialOrder A}} -> List A -> List A, то они между собой, возможноЮ не равны. Однако можно ввести специальный фактор-тип MList, отличающийся от List в точности тем, что (..., a, b, ...) и (..., b, a,...) считаются равными, когда a и b несравнимы с точки зрения частичного порядка O, то функции уже равны.
Теперь если свойства f действительно не зависят от порядка несравнимых элементов в результате сортировки, то результаты сортировки в соответствующих местах надо сохранять в переменные типа MList, а не List. И тогда все теоремы об f останутся верными при подмене одной сортировки на другую.
В HoTT есть фактортипы, типы где равенство может быть нетривиальным. В данном случае тип Eq MList имеет не только конструктор refl a = Eq MList a a, но и конструктор xchng, который переставляет местами несравнимые элементы, как я выше написал. В extensional ITT существуют сетоиды, но это жалкая замена левой руки, они примерно как .equals в Джаве/Скале, когда a.equals(b) совершенно не означает, что у a и b совпадают все наблюдаемые свойства.
____
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
sorhed: Только я не вижу проблемы с OTT. Что, она не может учесть равенства?
akuklev: В ней нет фактортипов. Там нет такой специальной конструкции, которая позволяет взять готовый тип и сказать «хочу такой же, только без крылышек». Ну то есть, другим equals. Сочетать хитрые фактортипы и конструктивность вообще тяжело. При помощи фактортипов например можно нараз сконструировать из последовательностей натуральных чисел действительные, а действительное число в общем случае нельзя точно записать, используя конечный объем памяти. Так что добавленин в теорию типов фактортипов тем или иным способом сразу делает её очень богатой: изниоткуда возникает разная топология — и теоретикомножественная, и алгебраическая.
А HoTT нужен на случай unstableSort'ов. Если у нас есть две не обязательно стабильных функции сортировки w и v: {A : Set} -> {{O : PartialOrder A}} -> List A -> List A, то они между собой, возможноЮ не равны. Однако можно ввести специальный фактор-тип MList, отличающийся от List в точности тем, что (..., a, b, ...) и (..., b, a,...) считаются равными, когда a и b несравнимы с точки зрения частичного порядка O, то функции уже равны.
Теперь если свойства f действительно не зависят от порядка несравнимых элементов в результате сортировки, то результаты сортировки в соответствующих местах надо сохранять в переменные типа MList, а не List. И тогда все теоремы об f останутся верными при подмене одной сортировки на другую.
В HoTT есть фактортипы, типы где равенство может быть нетривиальным. В данном случае тип Eq MList имеет не только конструктор refl a = Eq MList a a, но и конструктор xchng, который переставляет местами несравнимые элементы, как я выше написал. В extensional ITT существуют сетоиды, но это жалкая замена левой руки, они примерно как .equals в Джаве/Скале, когда a.equals(b) совершенно не означает, что у a и b совпадают все наблюдаемые свойства.
____
sorhed: Только я не вижу проблемы с OTT. Что, она не может учесть равенства?akuklev: В ней нет фактортипов. Там нет такой специальной конструкции, которая позволяет взять готовый тип и сказать «хочу такой же, только без крылышек». Ну то есть, другим equals. Сочетать хитрые фактортипы и конструктивность вообще тяжело. При помощи фактортипов например можно нараз сконструировать из последовательностей натуральных чисел действительные, а действительное число в общем случае нельзя точно записать, используя конечный объем памяти. Так что добавленин в теорию типов фактортипов тем или иным способом сразу делает её очень богатой: изниоткуда возникает разная топология — и теоретикомножественная, и алгебраическая.