December 6th, 2017

ДР Цертуса 2011

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

С тех пор, как в качестве побочного эффекта исследовательской программы Воеводского была решена проблема представления общерекурсивных (Тьюринг-полных) функций и вещественных чисел в теориях типов, ключевым вопросом является формализация теории самой унивалентной теории типов на языке унивалентной теории типов, и, говоря, шире представление в теориях типов квазикатегорий и аналогичных им высшекатегорных объектов — широчайший класс зависимых теорий типов находится, судя по всему, в соответствии с категориями обобщённо 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 не постулируется, а определяется по мере надобности индуктивно-рекурсивно.