Polimorfismo e tipos de dados indutivos

Estou curioso. Eu tenho trabalhado nesse tipo de dados no OCaml :

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

Que pode ser manipulado usando funções recursivas de tipo explícito (um recurso que foi adicionado recentemente). Exemplo:

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

Mas nunca fui capaz de defini-lo no 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 está choramingando. Não gosta do último construtor e diz algo que não entendo ou concordo completamente:

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

O que posso entender é que tipos indutivos que usam uma negação dentro de sua definição como type 'a term = Constructor ('a term -> …)são rejeitados, porque levariam a bestas feias e não fundamentadas, como termos λ (não tipados). No entanto, esse exptreetipo de dados em particular parece bastante inócuo: olhando para sua definição de OCaml , seu argumento 'anunca é usado em posições negativas.

Parece que Coq é cauteloso aqui. Então, existe realmente um problema com esse tipo de dados indutivo específico? Ou poderia Coq ser um pouco mais permissivo aqui?

Além disso, e os outros assistentes de prova, eles são capazes de lidar com uma definição tão indutiva (de uma maneira natural)?

Isso apareceu na lista de correspondência Coq várias vezes, mas nunca vi uma resposta conclusiva. Coq não é tão geral quanto poderia ser; as regras de (Coquand, 1990) e (Giménez, 1998) (e sua tese de doutorado) são mais gerais e não requerem estrita positividade. Positividade suficiente não é suficiente, porém, quando você sai Set; Este exemplo surgiu em várias discussões :

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

Com estruturas simples de dados como a sua, o tipo indutivo não causaria problemas além de tornar a implementação mais complexa.

$$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
.

Você pode definir valores e trabalhar com eles. Coq frequentemente será capaz de inferir o expoente. Set Implicit Argumentstornaria essas definições mais bonitas.

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)).

Eu acho que esse é o mesmo princípio proposto de uma forma mais geral por Ralph Mattes .

Referências

Thierry Coquand e Christine Paulin. Tipos definidos indutivamente . Em Proceedings of COLOG'88 , LNCS 417, 1990. [ Springer ] [ Google ]

Eduardo Giménez. Definições estruturais recursivas na teoria dos tipos . Na ICALP'98: Anais do 25º Colóquio Internacional sobre Autômatos, Idiomas e Programação. Springer-Verlag, 1998. [ PDF ]

Ralph Matthes descreve como simular tipos como este na Coq em "Uma estrutura de dados para poderes iterados" ( código , papel ).

Uma das primeiras coisas que a Coq faz é construir o princípio de indução associado ao tipo indutivo que você acabou de definir e entender o princípio de indução subjacente é um bom exercício.

Por exemplo, O : nat | S : nat -> natirá gerar o princípio de indução P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

Qual seria o princípio de indução correspondente iota? Parece que não há nenhum predicado Pque seria capaz de falar P te P (iota t), porque ele deve falar exptree a, exptree (exptree a), exptree (exptree (exptree a))...

Também o Omicronfaz a mesma coisa, mas o tipo é menor a cada vez. Você deve achar que ter uma referência tanto a um tipo menor quanto a um tipo maior tornaria as coisas confusas. (Dito isto, Omicroné o caminho certo)

Esse não é o critério exato que diz por que a definição não deve ser aceita, mas isso explica por que parece errado para mim.

exptreeParece que você está construindo uma gramática para expressões, coisa que geralmente não são que recursiva. Você quer ajuda com isso?