![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
akuklevВ интуиционистских теориях зависимых типов постулируется существование Π-, Σ-, 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 можно добавить счётно-бесконечный набор элементов-призраков, которые ведут себя как канонические элементы и не могут быть отличены от них наблюдениями, т.е. модели неизоморфны, но наблюдательно-неразличимы.)
Вселенные же не снабжены правилом расформирования, и это как раз потому, что автору никак не хочется ограничивать их, хочется работать в Open World Assumption, т.е. "мы предполагаем, что могут быть такие типы, которые мы не умеем описывать, и это не потому что у нас мало описательных средств, а просто потому что мир разнообразен". Вместо ограничения размера, для вселенных действует противоположный принцип: для типа T общего вида нельзя производить интроспекцию, типа "если этот тип равен Bool, делаем одно, если это Π-тип, делаем другое", т.к. во-первых могут быть типы неизвестных нам сортов, во вторых эквивалентность типов (т.е. вопрос, равен ли данный тип неизвестного сорта Bool'у) неразрешим. Этот принцип приводит к тому, что, например, единственная функция типа ∀T, T -> T, это ничего не делающая функция id. Для всевозможных типов отображений с универсальной квантификацией по типам получаются такого вида theorems for free, а общий принцип называется параметричностью.
Так вот давно существует идея что касательно вселенных в интуиционистских теориях типов следует ввести вместо правила расформирования правило универсальности, ту самую параметричность внутри теории сформулировать. Гипотеза, которая сейчас кружит в разных головах вокруг HoTT (= стандартная интуиционистская теория зависимых типов + аксиома унивалетности) состоит в том, что это правило универсальности это и есть вычислительная форма аксиомы унивалетности. Идея витает уже два года, но на конференции TYPES'15, которая будет через две недели, три или четыре доклада именно на эту тему.
(* Речь идёт об отличимости при помощи сколь угодно большого, но конечного числа наблюдений/измерений сколь угодно высокой, но конечной точности. Как известно (теорема Лёвенгейма — Скулема), во всякую модель бесконечной синтаксической алгебры вроде Nat можно добавить счётно-бесконечный набор элементов-призраков, которые ведут себя как канонические элементы и не могут быть отличены от них наблюдениями, т.е. модели неизоморфны, но наблюдательно-неразличимы.)
