Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Новости HoTT

На днях Altenkirch, Capriotti и Kraus (arxiv:1604.03799) выложили препринт о технике расширения HoTT предтипами (соответствующими в моделях нефибрантным объектам), и в особенности предтипом строгого равенства. Получившаяся теория типов имеет разрешимый тайпчекинг, и, судя по всему (доказательство разных тонких обещают скоро опубликовать в рамках диссертации Каприотти) является консервативным над HoTT. С одной стороны, так теряется одно из основных преимуществ HoTT — априорная non-evelness, т.е. “all grammatically correct properties of objects are invariant under isomorphism”. А в расширенной HoTT существуют “предсвойства”, которые вдоль изоморфизма не переносятся.

Зачем это расширение нужно? — для того, чтобы можно было определять структуры со строгим равенством, в особенности инфинитарные структуры вроде слабых (∞,1)-категорий так, как это делается в математике сейчас. С одной стороны, я не теряю надежды, что можно определить такие объекты и в полностью фибрантном расширении HoTT (включающем, однако, высшие коиндуктивные типы, чтобы можно было определить ∞-категории пользуясь подходом из “Weak ω-categories via terminal coalgebras“ Eugenia Cheng, Tom Leinster), с другой стороны расширение Альтенкирха сотоварищи нужно уже затем, чтобы отражать имеющиеся практики в математике, ну и главное, этот подход работает прямо сейчас, а не когда-нибудь, когда рак на горе свиснет и придумается правильное фибрантное расширение.

Вообще, я не верю в то, что judgemental equality в теории типов имеет семантический смысл, в частности потому что при определении теорий типов без суждений вида a ≡ b вполне можно обойтись, если использовать подход с двусторонним тайпчекингом (bi-directional typechecking), который на практике выглядит гораздо более естественным. Разумеется, задание всех правил двустороннего тайпчекинга даёт отношение “a можно подставить вместо b” на термах, и если два терма можно подставлять друг вместо друга в обе стороны, то их логично называть подстановочно равными. Однако это выглядит скорее как свойство термов, а не как свойство объектов, ими обозначаемых.
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.
  • 1 comment