Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Зачем нужны OTT (Observational Type Theory) и HoTT (Homotopic Type Theory)

Допустим у нас есть несколько ценных теорем о функции 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 совпадают все наблюдаемые свойства.

____
sorhed: Только я не вижу проблемы с OTT. Что, она не может учесть равенства?
akuklev: В ней нет фактортипов. Там нет такой специальной конструкции, которая позволяет взять готовый тип и сказать «хочу такой же, только без крылышек». Ну то есть, другим equals. Сочетать хитрые фактортипы и конструктивность вообще тяжело. При помощи фактортипов например можно нараз сконструировать из последовательностей натуральных чисел действительные, а действительное число в общем случае нельзя точно записать, используя конечный объем памяти. Так что добавленин в теорию типов фактортипов тем или иным способом сразу делает её очень богатой: изниоткуда возникает разная топология — и теоретикомножественная, и алгебраическая.
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.
  • 21 comments

  • (no subject)

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

  • Прогресс

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

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

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