Наследственное замещение с иерархией вселенной

11

Я читал о наследственной замене Простого лямбда-исчисления и Логической структуры с различными терминами и типами.

Мне интересно, есть ли примеры наследственного замещения в зависимо типизированной системе с иерархией юниверсов? то есть где и т. д.True:Set0:Set1:Set2

Мне интересно, в частности, как установить индукционную меру в такой системе. Версия с простым типом структурно уменьшается в типе заменяемой переменной. Это не работает с зависимыми типами, так как для LF бумага, которую я связал, использует просто набранное стирание терминов, выполняя наведение на форму типа.

Однако стирание в простые типы не работает с иерархией юниверсов, поскольку, если у вас есть что-то вроде этого:

  • f:(x:Set1)xTrue означает, что
  • f ((y:True)TrueTrue):TrueTrueTrue

т.е. применение функции привело к структурно большему типу.

Я предполагаю, что решение имеет какое-то отношение к индексам юниверса, но если существует существующая техника для установления того, что индукция обоснована, я бы предпочел цитировать ее, а не придумывать что-то самостоятельно.

jmite
источник

Ответы:

8

Вот ссылка на предикативную Систему F. Мера действительно включает в себя мультимножество уровней вселенных в типе. Я не могу сказать много о том, обобщает ли этот подход теорию предикативного зависимого типа.

Андраш Ковач
источник
8

По состоянию на ноябрь 2018 года, как это сделать для зависимых теорий типов с большими исключениями, остается открытым вопросом.

Установление того, что рекурсия обоснована, не так уж плохо; Вы можете использовать теорему Патараи, чтобы доказать, что заданная точка существует. См. Инструкции Роберта Харпера « Построение систем типов поверх операционной семантики» . (Вы также можете сделать это с помощью индуктивно-рекурсивного определения.)

Сложная часть - это на самом деле хорошая формулировка наследственной замены - естественное направление ведет вас к замене не одного термина, а полной замены контекста, и это вызывает много вопросов о том, когда и как устанавливать свойства вещей. как составы (наследственных) замен.

Если бы это оказалось невозможным, я был бы шокирован. Однако в настоящее время никто этого не сделал. Если вы хотите поработать над этим, я бы предложил связаться с Андреасом Абелем, Даном Ликата и Майком Шульманом. (Или я, в этом отношении.)

Нил Кришнасвами
источник
Не является ли сила согласованности теоремы о наследственных подстановках для теории типов с иерархией вселенной достаточно сильной? После того, как вы пройдете теорему, что еще нужно для получения согласованности теории?
Андрей Бауэр
1
@NeelKrishaswami: ты имеешь в виду, что это открытая проблема даже без иерархии вселенной? Сколько именно вы предполагаете о своей теории типов?
Андрей Бауэр
2
Второе недоразумение @ AndrejBauer: не содержит ли определение наследственной замены неявно аргумент завершения для сокращения хорошо типизированных терминов? Аргумент для простых типов, по-видимому, даже явно содержит порядок, который уменьшается при выполнении замещения, который является привередливым даже для Системы T (открыто, существует ли такой порядок для SN) и безнадежен для системы F.
cody
1
@AndrejBauer: если вы записываете наследственную операцию замещения, вы должны доказать, что она завершается, прежде чем вы действительно сможете назвать ее функцией. Доказательство завершения вряд ли будет ужасно трудным, поскольку можно показать, что MLTT со счетной иерархией юниверсов нормализуется с помощью интуитивистского ограниченного ZF. То, что открыто, на самом деле дает правильное определение наследственной операции замещения. Прямо сейчас неясно, является ли это трудной бюрократической проблемой, или трудной проблемой, которую можно остановить. У меня есть предчувствие, но кто на самом деле может сказать, не выполняя работу?
Нил Кришнасвами
1
@Blaisorblade: да, добавление больших исключений приводит к действительно большому скачку выразительной силы теории. Если у вас есть большие исключения, метатеория, в которой вы докажете последовательность / нормализацию, должна поддерживать индукцию-рекурсию как минимум.
Нил Кришнасвами