Lazi

Simplifier la récurrence ?

Contexte

Pour définir la règle de récurrence il faut une propriété (p), un point de départ (a) et une fonction "suivant" (next).
La règle de récurrence actuelle comporte la gestion de l'arrêt, pour cela la fonction "next" retourne un maybe.

Question

Est-il possible de se passer de la notion d'arrêt ?

Étude

Il faut une construction ou fonction pour le ou les éléments vérifiant p. La notion d'arrêt permet de se passer d'une construction qui serait elle-même sujette à des preuves par récurrence, que l'on ne pourrait probablement pas faire car on bouclerait sur les propriétés de la structure récursive portant les éléments vérifiant p.

Réponse

Non.