Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Category:

Типотеоретическое

С тех пор, как в качестве побочного эффекта исследовательской программы Воеводского была решена проблема представления общерекурсивных (Тьюринг-полных) функций и вещественных чисел в теориях типов, ключевым вопросом является формализация теории самой унивалентной теории типов на языке унивалентной теории типов, и, говоря, шире представление в теориях типов квазикатегорий и аналогичных им высшекатегорных объектов — широчайший класс зависимых теорий типов находится, судя по всему, в соответствии с категориями обобщённо Reedy-предпучков с дополнительной структурой или свойствами, см. напр. http://www.cs.nott.ac.uk/~psznk/docs/nicolai_highercatstruct_handout.pdf, https://arxiv.org/abs/1706.02866, https://arxiv.org/pdf/1703.03007.pdf.

Простейшим из возможных нетривиальных Reedy-предпучков являются семи-симплициальные типы. Разумеется, их можно построить, если вместо унивалентной теории типов взять теорию типов с двумя типами равенства (нормальным и “строгим”) и, соответственно, неунивалентными вселенными. Но это, конечно, от лукавого. На самом деле для решения этой задачи требуются лишь два ингридиента:
Индексированные индуктивно-индуктивные типы (https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/thesis/thesis.pdf), позволяющие определять башни типов
T[0] : *
T[1](t0 : T[0]) : *
T[2](t0 : T[0], t1 : T[1](t0)) : *
...

и придуманные Валерием Исаевым (двойственные высшим индиуктивным типом) records with conditions (точнее, indexed coinductive types with conditions), позволяющие строить из таких вот башен телескопические сигма-типы с когерентным равенством, те самые very dependent types.

* * *

Большие индуктивно-рекурсивные типы тоже интересны в контексте унивалентных ТТ интересны тем, что при помощи соопределяемой вместе с типом функции из этого типа в унивалентную вселенную, они в некотором смысле “прибивают гвоздями” равенство на типе (см. https://homotopytypetheory.org/2014/06/08/hiru-tdd/), что даёт слабые, но всё-таки надежды, что indexed coinductive types with conditions вообще-то можно представить при помощи достаточно крутых higher inductive-recursive types. Но до сих пор никому не удалось этого сделать, конечно же в том числе и мне.

Вообще же интерес к IR-типам у меня тоже в контексте автофагии. Дело в том, что IR- и только IR-типы позволяют определять внутри теории типов вселенные, замкнутые относительно формирования зависимых типов (зависимых сумм, произведений, индуктивных типов, малых индуктивно-рекурсивных типов). Конечно же сразу возникает вопрос, можно ли определить при помощи индукции-рекурсии вселенную, замкнутую относительно формирования больших IR-типов? Можно, конечно, постулировать такую вселенную (Mahlo universe), но её саму индуктивно-рекурсивно не определишь. Однако, если постулировать, то там внутри при помощи индукции-рекурсии можно определить иерархию вселенных Un, замкнутую относительно формирования “больших” (но влезающих в эту иерархию на конечном уровне) индуктивно-рекурсивных типов.
(Возможно, при наличии propositional resizing можно также показать сугубое существование (mere existence) Mahlo-вселенной |Uω|, следуя подходу статьи Антона Сетцера сотоварищи “An extended predicative definition of the Mahlo universe” и используя представимость Тьюринг-полных функций и возможность выделить среди них на уровне сугубого существования тотальные.)

В светлом будущем Pure Type Systems в духе Аарона Стумпа (см. предпредыдущий пост) хотелось бы видеть проблему large elimination решённой через такие вот индуктивно-рекурсивные типы. Т.е. систему, в которой Ambient Mahlo Universe представляет из себя не тип, а “собственный класс”, который не может являться элементом никакого другого типа или класса, а для индуктивно-рекурсивных типов есть особый конструктор типов, и счётная иерархия вселенных à la Martin-Löf не постулируется, а определяется по мере надобности индуктивно-рекурсивно.
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.
  • 9 comments