Les types inductifs sont des types définis en fonction d'eux-mêmes, par une définition auto-référentielle. Les algorithmes récursifs sont des algorithmes qui sont définis en fonction d'eux-mêmes, leurs définitions sont aussi auto-référentielles. Ce n'est donc pas un hasard si les types inductifs se manipulent particulièrement bien récursivement.
Le principe des algorithmes récursifs est toujours de calculer f v en utilisant le résultat de f v' pour des valeurs v' plus petites que v. Dans le contexte des types inductifs, plus petit signifie structurellement plus petit, v' est plus petit que v si v' est un sous-terme dans la construction de v.
Par exemple, la queue d'une liste est plus petite que la liste elle-même. Le sous-arbre gauche d'un arbre binaire est plus petit que l'arbre binaire tout entier. En reprenant la définition inductive des entiers naturels, on obtient le principe de récurrence, n est plus petit que Succ n.
Reprenons l'exemple des expressions arithmétiques.
Donnons une fonction pour évaluer une expression. Lorsqu'on travaille avec un type inductif, et qu'on ne sait pas comment écrire une fonction, un bon réflexe est d'observer la valeur, puis de réfléchir indépendamment à chaque cas :
Dans le premier cas, le résultat doit être la valeur de i. Dans le deuxième, c'est la somme de la valeur de expr1 et de la valeur de expr2. Ces deux valeurs peuvent être obtenues par un appel récursif. Le troisième cas est similaire au deuxième.
expr1 et expr2 sont dans les deux derniers cas des sous termes de l'expression observée, il est donc valide de rappeler eval récursivement sur ces deux valeurs.
Compliquons un peu l'exercice, en ajoutant des variables aux expressions arithmétiques.
Pour évaluer une telle expression, il faut attribuer une valeur à chaque variable, ce qui nous donne un contexte d'évaluation.
L'évaluation peut échouer si toutes les variables n'ont pas été définies. Nous allons écrire une fonction qui simplifie l'expression arithmétique autant que possible : si toutes les variables sont définies, on obtiendra un littéral contenant la valeur de l'expression pour ce contexte.
Que fait simplify, en particulier les cas 3 et 4 ? On simplifie les sous-expressions de l'expression à simplifier, et cela par appel récursif à simplify, puisque expr1 et expr2 sont bien des termes plus petits que l'expression observée. Ensuite, on vérifie si localement il est possible de simplifier l'expression, soit en additionnant deux litéraux, soit en les multipliant. On peut même ajouter des règles pour supprimer les additions par zéro, les multiplications par 0 ou 1 . (Notez comment il est possible de filtrer plusieurs cas en leur associant le même calcul).
