Definições recursivas sobre um tipo indutivo com componentes aninhados

Considere um tipo indutivo que possui algumas ocorrências recursivas em um local aninhado, mas estritamente positivo. Por exemplo, árvores com ramificação finita com nós usando uma estrutura de dados de lista genérica para armazenar os filhos.

Inductive LTree : Set := Node : list LTree -> LTree.

A maneira ingênua de definir uma função recursiva sobre essas árvores recorrendo sobre árvores e listas de árvores não funciona. Aqui está um exemplo com a sizefunção que calcula o número de nós.

Fixpoint size (t : LTree) : nat := match t with Node l => 1 + (size_l l) end
with size_l (l : list LTree) : nat := match l with
    | nil => 0
    | cons h r => size h + size_l r
  end.

Esta definição está incorreta (mensagem de erro extraída):

Error:
Recursive definition of size_l is ill-formed.
Recursive call to size has principal argument equal to
"h" instead of "r".

Por que a definição está mal formada, embora rseja claramente um subtermo de l? Existe uma maneira de definir funções recursivas nessa estrutura de dados?

---

Se você não é fluente na sintaxe Coq: LTreeé um tipo indutivo correspondente à seguinte gramática.

$$\begin{align} \mathtt{LTree} ::= & \\ \vert & \mathtt{list}(\mathtt{LTree}) \\ \end{align}$$

Tentamos definir a sizefunção por indução sobre árvores e listas. No OCaml, isso seria:

type t = Node of t list
let rec size = function Node l -> 1 + size_l l
and size_l = function [] -> 0
                    | h::r -> size h + size_l r

O que funciona

Se você aninhar a definição do ponto de correção nas listas dentro da definição do ponto de correção nas árvores, o resultado será bem digitado. Este é um princípio geral quando você aninha a recursão em um tipo indutivo, ou seja, quando a recursão passa por um construtor como list.

Fixpoint size (t : LTree) : nat :=
  let size_l := (fix size_l (l : list LTree) : nat :=
                  match l with
                    | nil => 0
                    | h::r => size h + size_l r
                  end) in
  match t with Node l =>
    1 + size_l l
  end.

Ou se você preferir escrever isso de forma mais concisa:

Fixpoint size (t : LTree) : nat :=
  match t with Node l =>
    1 + (fix size_l (l : list LTree) : nat :=
          match l with
            | nil => 0
            | h::r => size h + size_l r
          end) l
  end.

(Não tenho idéia de quem o ouvi primeiro; isso certamente foi descoberto de forma independente várias vezes.)

Um predicado geral de recursão

De um modo mais geral, você pode definir o princípio de indução “adequado” LTreemanualmente. O princípio de indução gerado automaticamente LTree_rectomite a hipótese da lista, porque o gerador do princípio de indução apenas entende ocorrências estritamente positivas não aninhadas do tipo indutivo.

LTree_rect = 
fun (P : LTree -> Type) (f : forall l : list LTree, P (Node l)) (l : LTree) =>
match l as l0 return (P l0) with
| Node x => f x
end
     : forall P : LTree -> Type,
       (forall l : list LTree, P (Node l)) -> forall l : LTree, P l

Vamos adicionar a hipótese de indução nas listas. Para cumpri-lo na chamada recursiva, chamamos o princípio de indução de lista e passamos a ele o princípio de indução de árvore na árvore menor dentro da lista.

Fixpoint LTree_rect_nest (P : LTree -> Type) (Q : list LTree -> Type)
                         (f : forall l, Q l -> P (Node l))
                         (g : Q nil) (h : forall t l, P t -> Q l -> Q (cons t l))
                         (t : LTree) :=
  match t as t0 return (P t0) with
    | Node l => f l (list_rect Q g (fun u r => h u r (LTree_rect_nest P Q f g h u)) l)
  end.

Por quê

A resposta para o motivo está nas regras precisas para aceitar funções recursivas. Essas regras são forçosamente sutis, porque existe um delicado equilíbrio entre permitir casos complexos (como este, com recursão aninhada no tipo de dados) e insatisfação. O manual de referência da Coq apresenta a linguagem (o cálculo de construções indutivas, que é a linguagem de prova da Coq), principalmente com definições formalmente precisas, mas se você deseja as regras exatas sobre indução e coindução, precisará ir aos documentos de pesquisa, neste tópico de Eduardo Giménez [1].

Fix$\mathsf{Fix} f_i \, \{ f_1 : A_1 := t_1 \; ; \;\; f_2 : A_2 := t_2 \}$

$$\begin{align*} \Gamma_1 &= (x : \mathtt{LTree}) & A_1 &= \mathrm{nat} & t_1 &= \mathsf{case}(x, \mathtt{LTree}, \lambda y. g_1 (f_2 y)) \\ \Gamma_2 &= (l : \mathtt{list}\;\mathtt{LTree}) & A_2 &= \mathrm{nat} & t_2 &= \mathsf{case}(l, \mathtt{list \: LTree}, \lambda h \: r. g_2 (f_1 h) (f_2 r)) \\ \end{align*}$$

$f_j$$t_i$$f_i$

• $i=1$$j=2$ltsize
• $i=2$$j=1$hlsize_l
• $i=2$$j=2$rlsize_l

A razão pela qual hnão é estruturalmente menor do que, lsegundo o intérprete Coq, não está clara para mim. Tanto quanto eu entendo das discussões na lista Coq-club [1] [2], esta é uma restrição no intérprete, que em princípio poderia ser levantada, mas com muito cuidado para evitar a introdução de uma inconsistência.

Referências

Cocorico, o wiki Coq não-determinante: Indução Mútua

Lista de discussão Coq-Club:

• [1] Tópico "Meta-teoria: indução sobre termos com variáveis ​​abstratas"; primeira mensagem por Robbert Krebbers em 21-10-2009; explicação de Adam Chlipala ; contra-exemplo de Bruno Barras ; resposta de Hugo Herbelin .
• [2] Tópico "Verificação de término com recursão aninhada"; primeira mensagem de Gert Smolka; resposta de Hugo Herbelin.

A equipe de desenvolvimento da Coq. O Coq Proof Assistant: Manual de Referência . Versão 8.3 (2010). [ web ] cap. 4 .

Eduardo Giménez. Codificando definições guardadas com esquemas recursivos . Em Types'94: Types for Proofs and Programs , LNCS 996. Springer-Verlag, 1994. doi: 10.1007 / 3-540-60579-7_3 [ Springer ]

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 ]

Obviamente, esse é um problema específico da Coq, pois acredito que existem maneiras mais agradáveis ​​de contornar isso com outros assistentes de provas (estou olhando para a Agda)

A princípio, pensei que rnão era reconhecido estruturalmente menor porque a estrutura é apenas sobre a definição indutiva atualmente manipulada Fixpoint: portanto, este não é um LTreesubtermo, mesmo que seja listsubtermo.

Mas se você expandir o processamento da lista, funcionará:

Fixpoint size t :=
  match t with
  | Node l => S
     ((fix size_l l :=
     match l with
     | nil => 0
     | cons t l => size_l l + size t
     end) l)
 end.

Ou como a função auxiliar já existe na biblioteca padrão:

Require Import List.

Fixpoint size t :=
  match t with
  | Node l => S (fold_left (fun a t => a + size t) l 0)
  end.

Para ser sincero, não sei por que esses são aceitos pela Coq, mas estou feliz por serem.

Há também uma solução que funciona com mais frequência e não apenas para listas: definindo um tipo indutivo independente. Nesse caso, você pode definir sua sizefunção manualmente. (com dois pontos de fixação)

Inductive LTree : Set :=
  | Node : list_LTree -> LTree
with list_LTree : Set :=
  | LTree_nil : list_LTree
  | LTree_cons : LTree -> list_LTree -> list_LTree.

Observe que se você tiver problemas para definições indutivas mais complexas, poderá usar um argumento de diminuição de tamanho. Isso é possível, mas complicado para esse problema (e eu ousaria dizer a maioria dos problemas)