Полиморфизм и индуктивные типы данных

Мне любопытно. Я работал над этим типом данных в OCaml :

type 'a exptree =
  | Epsilon
  | Delta of 'a exptree * 'a exptree
  | Omicron of 'a
  | Iota of 'a exptree exptree

Которым можно манипулировать, используя явно типизированные рекурсивные функции (функция, которая была добавлена ​​совсем недавно). Пример:

let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
  fun f ->
    begin function
    | Epsilon -> Epsilon
    | Delta (t1, t2) -> Delta (map f t1, map f t2)
    | Omicron t -> Omicron (f t)
    | Iota tt -> Iota (map (map f) tt)
    end

Но я никогда не мог определить это в Coq :

Inductive exptree a :=
  | epsilon : exptree a
  | delta : exptree a -> exptree a -> exptree a
  | omicron : a -> exptree a
  | iota : exptree (exptree a) -> exptree a
.

Coq скулит. Ему не нравится последний конструктор, и он говорит что-то, с чем я не совсем понимаю или с чем не согласен:

Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".

Что я могу понять, так это то, что индуктивные типы, использующие отрицание внутри своего определения, как type 'a term = Constructor ('a term -> …), отвергнуты, потому что они приведут к уродливым необоснованным животным, таким как (нетипизированные) λ-члены. Однако этот конкретный exptreeтип данных выглядит достаточно безобидным: если смотреть на его определение OCaml , его аргумент 'aникогда не используется в отрицательных позициях.

Кажется, что Coq здесь слишком осторожен. Так есть ли действительно проблема с этим конкретным индуктивным типом данных? Или Coq может быть немного более разрешающим здесь?

Кроме того, как насчет других помощников по доказательству, способны ли они справиться с таким индуктивным определением (естественным образом)?

Это попадало в список рассылки Coq несколько раз, но я никогда не видел окончательного ответа. Coq не такой общий, как мог бы; правила в (Coquand, 1990) и (Giménez, 1998) (и его кандидатская диссертация) являются более общими и не требуют строгой позитивности. Однако достаточно позитива недостаточно, когда вы выходите на улицу Set; этот пример возник в нескольких дискуссиях :

Inductive Big : Type := B : ((B -> Prop) -> Prop) -> Big.

С такими простыми структурами данных, как ваша, индуктивный тип не вызовет других проблем, кроме как усложнит реализацию.

$$F = \epsilon + \delta\, (F \times F) + \omicron\, \mathrm{id} + F \circ F$$

$\mathrm{exptree} : a \mapsto \mathrm{exptree}(a)$$\mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree} \circ \mathrm{exptree}, \ldots$$\mathrm{exptree}^0(a) = a$$\mathrm{exptree}^1(a) = \mathrm{exptree}(a)$$\mathrm{exptree}^2(a) = \mathrm{exptree}(\mathrm{exptree}(a))$$a$$\mathrm{exptree}^0(a) = a$

Inductive et : nat -> Type -> Type :=
  | alpha : forall a, a -> et 0 a                      (*injection*)
  | omicron : forall n a, et n a -> et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -> et (S n) a -> et (S n) a
  | iota : forall n a, et (S (S n)) a -> et (S n) a
.

Вы можете приступить к определению ценностей и работе над ними. Coq часто сможет вывести показатель степени. Set Implicit Argumentsсделает эти определения красивее.

Definition exptree := et 1.
Definition et1 : exptree nat :=
  delta _ _ (omicron _ _ (alpha _ 42)) (epsilon _ _).
Definition et2 : exptree nat := iota _ _ (omicron _ _ et1).

exptreeet 0S n$a$$a$

Inductive et : nat -> Type -> Type :=
  | omicron_0 : forall a, a -> et 0 a
  | omicron_S : forall n a, et n a -> et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -> et n a -> et n a
  | iota : forall n a, et (S n) a -> et n a
.
Definition exptree := et 0.
Definition et1 : exptree nat :=
  delta _ _ (omicron_0 _ 42) (epsilon _ _).
Definition et2 : exptree nat :=
  (iota _ _ (omicron_S _ _ et1)).

Я думаю, что это тот же принцип, предложенный в более общей форме Ральфом Маттесом .

Ссылки

Тьерри Кокванд и Кристина Полин. Индуктивно определяемые типы . В Слушаниях COLOG'88 , LNCS 417, 1990. [ Springer ] [ Google ]

Эдуардо Хименес. Структурно-рекурсивные определения в теории типов . В ICALP'98: Материалы 25-го Международного коллоквиума по автоматам, языкам и программированию. Springer-Verlag, 1998. [ PDF ]

Ральф Мэттс (Ralph Matthes) описывает, как моделировать типы, подобные этому, в Coq в «Структуре данных для повторяющихся полномочий» ( код , статья ).

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

Например O : nat | S : nat -> natбудет генерировать принцип индукции P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

Какому принципу индукции соответствует iota? Кажется , что нет никакого предиката , Pкоторый был бы в состоянии говорить о P tи P (iota t), так как он должен говорить о exptree a, exptree (exptree a), exptree (exptree (exptree a))...

Также Omicronделает то же самое, но тип меньше с каждым разом. Вы должны чувствовать, что наличие ссылки как на меньший, так и на больший тип может привести к путанице. (Тем не менее, Omicronэто правильный путь)

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

exptreeКажется , что вы строите грамматику для выражений, вещь, как правило , не является , что рекурсивными. Вы хотите помочь с этим?