Имеет ли значение порядок объявлений в индуктивном типе?

9

Мне было интересно, может ли порядок объявлений индуктивного типа иметь значение.

Например, в Coq вы можете определить Natлибо:

Inductive Nat :=
  | O : Nat
  | S : Nat -> Nat.

или

Inductive Nat :=
  | S : Nat -> Nat
  | O : Nat.

Возможно, это изменит порядок параметров в автоматически сгенерированном элиминаторе, но это не имеет большого значения.

Что мне интересно, так это то, можно ли написать декларацию

Inductive typewhereordermatters :=
  | cons1 : type1
  | cons2 : type2.

где type2зависимый тип, в зависимости от cons1? (и в этом случае запись объявлений в другом порядке не будет иметь никакого смысла, поскольку type2будет ссылаться на то, cons1чего еще не существует).

lo.logic type-theory coq dependent-type Гийом Брунери
источник

Ответы:

10

  1. Порядок не имеет значения. Я не могу придумать случай, когда это будет. Как отмечает в комментарии Андрей Бауэр , при изменении порядка результат канонически изоморфен оригиналу .

  2. Один случай не может зависеть от другого случая. Элементы суммы представляют выбор, поэтому не имеет смысла, что выбор зависит от выбора, который не был сделан.

Дэйв Кларк
источник
2
Вы можете быть более точным в своем первом пункте. Порядок не имеет значения. Если вы измените порядок, результат канонически изоморфен оригиналу.
Андрей Бауэр
2
@Dave: Спасибо! Я задавал этот вопрос из-за (очень экспериментальной теории) высших индуктивных типов, где это явление, по- видимому, происходит , и я хотел знать, может ли это быть и в случае регулярных индуктивных типов.
Гийом Брунери
1
@Guillaume: Я не уверен, на какое явление вы указываете по ссылке. Различные предложения конструктора определения типа данных не могут зависеть друг от друга, независимо от того, является ли это типом данных более высокого порядка. Возможно, вы думаете о зависимых записях (которые используются по ссылке и доступны в Agda и Coq )?
Ноам Цайлбергер
1
@Noam: в примере с более высоким индуктивным типом circleтип loopконструктора зависит от baseконструктора.
Гийом Брунери
2
@Guillaume: я вижу сейчас (они вводят экспериментальный синтаксис), не знаю, как я пропустил это.
Ноам Цайлбергер
6

Имеет ли значение заказ, как вы просите? Нет.

Но порядок совершенно не имеет отношения к функционированию помощника доказательства? Опять нет. В Matita, ассистенте доказательства, очень похожем на Coq, порядок, в котором конструкторы записываются в индуктивном определении, имеет значение для проверки типа, особенно при проверке типа выражения соответствия.

Сначала Матита должен проверить, сопоставляются ли все конструкторы в теле совпадения. Это делается путем циклического перебора конструкторов в порядке их объявления. Затем идет проверка типа собственно выражения соответствия, что происходит в обратном порядке, сначала проверяется регистр для последнего объявленного конструктора. Этот тип затем проводится и используется для проверки других случаев.

Это очень часто обнаруживается при написании выражения большого соответствия. Сначала вы должны заполнить простые случаи, оставляя сложные случаи под символом подстановки, периодически проверяя написанное, чтобы убедиться, что это имеет смысл. Иногда Матита не может определить тип выражения неполного совпадения, но вполне с радостью сделает это, если заполнить регистр для последнего конструктора, определенного в индуктивном типе.

Я предполагаю, хотя я не уверен, что Coq делает что-то подобное.

Доминик Маллиган
источник