Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Почему унивалентность хотят связать с параметричностью

В интуиционистских теориях зависимых типов постулируется существование Π-, Σ-, W-, а также той или иной иерархии вселенных Ui. Так вот все из них, кроме вселенных, комплектуются как правилами формирования, так и правилами расформирования. Правила формирования это например конструкторы Pair(a, b) для пары, конструкторы Zero и Succ(pred) для натуральных чисел, ламбда-выражения для Π-типов. А правила расформирования (разкарривание для пары, индукция для натуральных чисел) кроме их практического применения несут посыл, что пара не содержит ничего кроме двух элементов, которые в неё засунули, всякое натуральное число это либо Zero, либо применённый к нему конечное число раз Succ, иными словами размер алгебр Nat, Pair и т.д. фиксируется сверху, правила расформирования запрещают чтобы там были элементы отличимые* от канонических.

Вселенные же не снабжены правилом расформирования, и это как раз потому, что автору никак не хочется ограничивать их, хочется работать в Open World Assumption, т.е. "мы предполагаем, что могут быть такие типы, которые мы не умеем описывать, и это не потому что у нас мало описательных средств, а просто потому что мир разнообразен". Вместо ограничения размера, для вселенных действует противоположный принцип: для типа T общего вида нельзя производить интроспекцию, типа "если этот тип равен Bool, делаем одно, если это Π-тип, делаем другое", т.к. во-первых могут быть типы неизвестных нам сортов, во вторых эквивалентность типов (т.е. вопрос, равен ли данный тип неизвестного сорта Bool'у) неразрешим. Этот принцип приводит к тому, что, например, единственная функция типа ∀T, T -> T, это ничего не делающая функция id. Для всевозможных типов отображений с универсальной квантификацией по типам получаются такого вида theorems for free, а общий принцип называется параметричностью.

Так вот давно существует идея что касательно вселенных в интуиционистских теориях типов следует ввести вместо правила расформирования правило универсальности, ту самую параметричность внутри теории сформулировать. Гипотеза, которая сейчас кружит в разных головах вокруг HoTT (= стандартная интуиционистская теория зависимых типов + аксиома унивалетности) состоит в том, что это правило универсальности это и есть вычислительная форма аксиомы унивалетности. Идея витает уже два года, но на конференции TYPES'15, которая будет через две недели, три или четыре доклада именно на эту тему.


(* Речь идёт об отличимости при помощи сколь угодно большого, но конечного числа наблюдений/измерений сколь угодно высокой, но конечной точности. Как известно (теорема Лёвенгейма — Скулема), во всякую модель бесконечной синтаксической алгебры вроде Nat можно добавить счётно-бесконечный набор элементов-призраков, которые ведут себя как канонические элементы и не могут быть отличены от них наблюдениями, т.е. модели неизоморфны, но наблюдательно-неразличимы.)
Tags: fprog
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