Définitions récursives sur un type inductif avec des composants imbriqués

Considérons un type inductif qui a des occurrences récursives dans un emplacement imbriqué, mais strictement positif. Par exemple, des arbres à ramifications finies avec des nœuds utilisant une structure de données de liste générique pour stocker les enfants.

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

La manière naïve de définir une fonction récursive sur ces arbres en récursant sur les arbres et les listes d'arbres ne fonctionne pas. Voici un exemple avec la sizefonction qui calcule le nombre de nœuds.

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.

Cette définition est mal formée (message d'erreur extrait):

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

Pourquoi la définition est-elle mal formée, même si elle rest clairement un sous-terme de l? Existe-t-il un moyen de définir des fonctions récursives sur une telle structure de données?

---

Si vous ne maîtrisez pas la syntaxe Coq: LTreeest un type inductif correspondant à la grammaire suivante.

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

Nous essayons de définir la sizefonction par induction sur des arbres et des listes. Dans OCaml, ce serait:

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

Ce qui fonctionne

Si vous imbriquez la définition du point fixe sur des listes à l'intérieur de la définition du point fixe sur les arbres, le résultat est bien typé. Il s'agit d'un principe général lorsque vous avez imbriqué la récursivité dans un type inductif, c'est-à-dire lorsque la récursivité passe par un constructeur comme 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 si vous préférez écrire ceci de façon plus laconique:

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.

(Je n'ai aucune idée de qui je l'ai entendu en premier; cela a certainement été découvert plusieurs fois de manière indépendante.)

Un prédicat général de récursivité

Plus généralement, vous pouvez définir LTreemanuellement le principe d'induction «correct» . Le principe d'induction généré automatiquement LTree_rectomet l'hypothèse de la liste, car le générateur de principe d'induction ne comprend que les occurrences strictement positives non imbriquées de type inductif.

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

Ajoutons l'hypothèse d'induction sur les listes. Pour le remplir dans l'appel récursif, nous appelons le principe d'induction de liste et lui passons le principe d'induction d'arbre sur le plus petit arbre à l'intérieur de la liste.

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.

Pourquoi

La réponse à cette question réside dans les règles précises d'acceptation des fonctions récursives. Ces règles sont forcément subtiles, car il y a un équilibre délicat entre autoriser des cas complexes (comme celui-ci, avec une récursion imbriquée dans le type de données) et des anomalies. Le manuel de référence Coq présente le langage (le calcul des constructions inductives, qui est le langage de preuve de Coq), principalement avec des définitions formellement précises, mais si vous voulez les règles exactes concernant l'induction et la coinduction, vous devrez consulter les articles de recherche, sur ce sujet 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

La raison pour laquelle hn'est pas structurellement plus petit que lselon l'interprète Coq n'est pas claire pour moi. D'après ce que je comprends des discussions sur la liste des Coq-clubs [1] [2], il s'agit d'une restriction dans l'interprète, qui pourrait en principe être levée, mais très soigneusement pour éviter d'introduire une incohérence.

Les références

Cocorico, le wiki Coq non terminal: induction mutuelle

Liste de diffusion Coq-Club:

• [1] Discussion «Méta-théorie: induction sur des termes avec des variables abstraites»; premier message de Robbert Krebbers le 21/10/2009; explication d'Adam Chlipala ; contre-exemple de Bruno Barras ; réponse de Hugo Herbelin .
• [2] Discussion «Vérification de terminaison avec récursivité imbriquée»; premier message de Gert Smolka; réponse de Hugo Herbelin.

L'équipe de développement Coq. Assistant Coq Proof: Manuel de référence . Version 8.3 (2010). [ web ] ch. 4 .

Eduardo Giménez. Codification des définitions gardées avec des schémas récursifs . Dans Types'94: Types pour les épreuves et les programmes , LNCS 996. Springer-Verlag, 1994. doi: 10.1007 / 3-540-60579-7_3 [ Springer ]

Eduardo Giménez. Définitions structurelles récursives en théorie des types . In ICALP'98: Actes du 25e Colloque international sur les automates, les langues et la programmation. Springer-Verlag, 1998. [ PDF ]

C'est évidemment un problème spécifique à Coq car je pense qu'il existe de meilleures façons de le contourner avec d'autres assistants de preuve (je regarde Agda)

Au début, je pensais que ce rn'était pas reconnu comme étant structurellement plus petit parce que la structure ne concerne que la définition inductive actuellement gérée par Fixpoint: ce n'est donc pas un sous- LTreeterme même si c'est un sous- listterme.

Mais si vous développez le traitement de la liste, cela fonctionne:

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 puisque la fonction auxiliaire existe déjà dans la bibliothèque standard:

Require Import List.

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

Pour être honnête, je ne sais pas pourquoi ceux-ci sont acceptés par Coq, mais je suis sûr qu'ils le sont.

Il existe également une solution qui fonctionne plus souvent et pas seulement pour les listes: définir un type inductif autonome. Dans ce cas, vous pouvez définir votre sizefonction manuellement. (avec deux points fixes)

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

Notez que si vous rencontrez des problèmes pour des définitions inductives plus complexes, vous pouvez utiliser un argument de diminution de taille. C'est possible mais lourd pour ce problème (et j'oserais dire pour la plupart des problèmes)