Polimorfizm i indukcyjne typy danych

Jestem ciekawy. Pracowałem nad tym typem danych w OCaml :

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

Z którymi można manipulować za pomocą jawnie wpisanych funkcji rekurencyjnych (funkcja dodana całkiem niedawno). Przykład:

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

Ale nigdy nie byłem w stanie zdefiniować tego w 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 marudzi. Nie lubi ostatniego konstruktora i mówi coś, czego nie do końca rozumiem lub z czym się nie zgadzam:

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

Mogę zrozumieć, że typy indukcyjne wykorzystujące negację w swojej definicji, takie jak, type 'a term = Constructor ('a term -> …)są odrzucane, ponieważ doprowadziłyby do brzydkich, nieuzasadnionych bestii, takich jak (nietypowane) terminy λ. Jednak ten szczególny exptreetyp danych wydaje się wystarczająco nieszkodliwy: patrząc na jego definicję OCaml , jego argument 'anigdy nie jest stosowany w pozycjach ujemnych.

Wygląda na to, że Coq jest tutaj zbyt ostrożny. Czy naprawdę istnieje problem z tym konkretnym rodzajem danych indukcyjnych? A może Coq może być tu nieco bardziej liberalny?

A co z innymi asystentami dowodowymi, czy są w stanie poradzić sobie z taką indukcyjną definicją (w naturalny sposób)?

To pojawiało się na liście mailingowej Coq kilka razy, ale nigdy nie widziałem rozstrzygającej odpowiedzi. Coq nie jest tak ogólny, jak mógłby być; zasady w (Coquand, 1990) i (Giménez, 1998) (i jego rozprawa doktorska) są bardziej ogólne i nie wymagają ścisłej pozytywności. Wystarczająca pozytywność nie wystarczy jednak, gdy wychodzisz na zewnątrz Set; ten przykład pojawił się w kilku dyskusjach :

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

W przypadku zwykłych struktur danych, takich jak Twoja, typ indukcyjny nie powodowałby innych problemów niż skomplikowanie implementacji.

Istnieje ogólny sposób definiowania typów takich jak ten zdefiniowany jako punkt stały wielomianu:

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

Zamiast próby zdefiniowania funkcji , zdefiniuj rodzinę typów . Oznacza to dodanie parametru liczbowego do typu, który koduje liczbę samodzielnych kompozycji ( , , itp.) oraz dodatkowy konstruktor wstrzykiwania, aby zamienić w .$\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)$a e x p t r e e 0 ( 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
.

Możesz przejść do definiowania wartości i pracować nad nimi. Coq często będzie w stanie wywnioskować wykładnik potęgi. Set Implicit Argumentssprawiłoby, że te definicje byłyby ładniejsze.

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

Może wolisz zmniejszyć argument o 1, więc tak exptreejest et 0. Eliminuje to wiele S nw definicji, które mogą wprowadzić pewne dowody łatwiejsze, ale wymaga podzielenia początkową sprawę od przypadku nawrotu każdej konstruktora, która pobiera argument (zamiast dodawania jednego konstruktora wtrysku dla ). W tym przykładzie jest tylko jeden konstruktor do podzielenia, więc powinien to być dobry wybór.$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)).

Myślę, że jest to ta sama zasada zaproponowana w bardziej ogólnej formie przez Ralpha Mattesa .

Bibliografia

Thierry Coquand i Christine Paulin. Indukcyjnie zdefiniowane typy . W Proceedings of COLOG'88 , LNCS 417, 1990. [ Springer ] [ Google ]

Eduardo Giménez. Strukturalne definicje rekurencyjne w teorii typów . W ICALP'98: Materiały z 25. Międzynarodowego Kolokwium na temat automatów, języków i programowania. Springer-Verlag, 1998. [ PDF ]

Ralph Matthes opisuje, jak symulować takie typy w Coq w „A Datastructure for Iterated Powers” ​​( kod , papier ).

Jedną z pierwszych rzeczy, które robi Coq, jest zbudowanie zasady indukcji związanej z właśnie zdefiniowanym typem indukcji i zrozumienie podstawowej zasady indukcji jest dobrym ćwiczeniem.

Na przykład O : nat | S : nat -> natwygeneruje zasadę indukcji P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

Jaka byłaby zasada indukcji iota? Wydaje się, że nie ma orzeczenie P, które będzie w stanie o tym mówić P ti P (iota t), ponieważ powinien mówić o exptree a, exptree (exptree a), exptree (exptree (exptree a))...

To samo Omicronrobi to samo, ale typ jest za każdym razem mniejszy. Powinieneś czuć, że odniesienie zarówno do mniejszego, jak i większego typu spowodowałoby bałagan. (To powiedziawszy, Omicronto właściwa droga)

To nie są dokładne kryteria, które mówią, dlaczego definicja nie powinna zostać zaakceptowana, ale to wyjaśnia, dlaczego wydaje mi się to niewłaściwe.

exptreewygląda na to, że budujesz gramatykę wyrażeń, co na ogół nie jest tak rekurencyjne. Czy chcesz w tym pomóc?