Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Очень-очень интересно!

В предикативных типизированных исчислениях построений встречаются много разных способов определять типы, самый универсальный предикативный (т.е. избегающей неразрешимой рекурсии) известный на сегодня способ определять типы — расслоенные индуктивно-рекурсивные определения, таким образом можно определять не только индексированные контейнеры (эквивалентно: индуктивные семейства типов), их зависимые суммы и произведения, но и вселенные (типы типов), замкнутые относительно построения в них индексированных контейнеров, зависимых сумм и произведений. В общем это такой зверь, которого достаточно для всех известных применений, не считая высших типов. Именно индуктивно-рекурсивно (и заведомо только так) можно построить модель зависимо-типизированного языка в нём самом, т.е. пару из зависимого типа Expr[T] (валидное выражение языка типа T) и функции execute: Expr[T] => T.

Ничего нормального для высших типов на эту тему ещё не изобрели, в частности в HoTT стоит адова проблема построения симплициалных типов (это важно потому что показано, что если в HoTT можно смоделировать её саму, то с необходимостью можно сэмулировать и симплициальные типы). С другой стороны, с колокольни HoTT вообще непонятно, как могут строиться в одномерной теории вселенные типов, доказано что уважающая унивалентность вселенная n-типов в HoTT неизбежно имеет h-уровень больше n. То есть понятно, что индукция-рекурсия очень поверхностно совместима с HoTT, унивалентных вселенных так не построишь, да и другие интересности получаются неэквивариантными.

В недавней статье Neil Ghani et al. вводят очень интересную (красивую с категорной точки зрения) положительную индукцию-рекурсию: https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/papers/positive_calco2013.pdf.
Крайне интересным образом, вселенная, замкнутая относительно построения П-типов, методами IR+ не получишь, однако можно получить группоид, обладающий нужными свойствами, это как раз то что в HoTT должно получиться. Наверняка за этим делом скрывается обобщение – некая высшая положительная индукция-рекурсия HIR+, методами которой можно как раз получать всякие там симплициальные типы.
Subscribe

  • Прогресс

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

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

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

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • 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.
  • 6 comments