Depuis son ouverture sur les différents secteurs de la vie courante, l’informatique nous a permis de rouler des véhicules sans conducteur, de déplacer des robots sur Mars, d’assister des séances de chirurgie par des robots, de gérer des bases des données de banques, etc. En effet, la liste des applications assistées par ordinateur est devenue innombrable. Des applications critiques, telles que nous avons cité, mettent en jeu des ressources humaines, matérielles et financières importantes. La vérification que ces systèmes informatiques accomplissent leurs rôles souhaités en utilisant des méthodes basées sur des notions mathématiques et logiques, appelées méthodes formelles  , est fortement recommandée. Ces méthodes permettent de définir un système, de décrire ses propriétés et d’établir leurs preuves de validation dans le même environnement formel. Ces preuves se construisent formellement et conformément à la description du système.

Ancien sujet mathématique et philosophique, la théorie de la preuve joue de nos jours un rôle important en informatique, notamment pour le développement des logiciels critiques. Elle permet d’étudier les preuves en tant qu’objets formels. Jadis, on se contentait des preuves développées par l’homme. De nos jours, ces preuves sont devenues grandes et portent sur des systèmes de taille industrielle. L’homme est devenu incapable de les certifier et est remplacé par l’ordinateur.

Le raisonnement par récurrence est parmi les raisonnements mathématiques les plus adéquats pour le traitement des structures des données ou des fonctions récursivement définies. Les premières traces de ce raisonnement remontent à la philosophie grecque :

« De l’induction, son importance égale à celle du syllogisme  [. . .] ; l’induction est plus évidente que le syllogisme » Le premier maître  [Saint-Hilaire1843]. Depuis, il est utilisé par plusieurs mathématiciens et philosophes dans le monde oriental et occidental. Des mathématiciens comme Al-Karkhi  , Pascal  et Fermat  ont utilisé ce raisonnement pour résoudre des problèmes mathématiques [Al-Karkhi et Woepcke1853, Pascal et Lafuma1963, Brassinne1853]. D’autres savants l’ont considéré parmi les ressources de développement des mathématiques et de toutes les sciences.

« Si les mathématiques n’en avaient pas d’autre elles seraient donc tout de suite arrêtées dans leur développement ; mais elles ont de nouveau recours au même procédé, c’est-à-dire au raisonnement par récurrence et elles peuvent continuer leur marche en avant.

Raisonnement par récurrence noethérienne

Fréquemment utilisé dans la théorie de la preuve, le principe général de raisonnement par récurrence est le suivant : une proposition P définie sur un ensemble d’éléments E est vraie s’il existe une démonstration que cette proposition est vraie pour tout élément x de E en supposant qu’elle l’est pour tous les éléments plus petits que x . On dit que la proposition est montrée vraie par récurrence. Ce principe ne peut être appliqué que sur des ensembles d’éléments noethériens munis d’ordres de récurrence qu’on note par <. D’une façon formelle, on définit le principe général de récurrence noethérienne comme suit :
(RN ) : (∀y ∈ E,(∀ z ∈ E, z < y ⇒ P(z )) ⇒ P(y)) ⇒ ∀x ∈ E,P(x ).

L’application du principe RN sur l’ensemble E distingue les instances de P qui jouent le rôle des conclusions de récurrence, telles que (P(y), ∀y ∈ E), et celles qui sont des hypothèses de récurrence, telles que P(z ), ∀z ∈ E, z < y. La relation établie entre toutes les conclusions et leurs hypothèses de récurrence est nommée un schéma de récurrence. Ce schéma contient des cas de base qui n’ont pas d’hypothèses de récurrence, et des cas de récurrence qui en ont.

Correction des preuves par récurrence noethérienne 

La correction de la preuve par récurrence noethérienne dépend fortement de l’ordre de récurrence noethérienne. En effet, la preuve par récurrence d’une proposition P ne peut être considérée comme correcte que si l’ordre < est noethérien, i.e. garantit qu’il n’existe aucune séquence d’éléments de ε infiniment décroissante. La vérification de la correction de ces preuves consiste à la vérification que toute hypothèse de récurrence introduite est plus petite que sa conclusion.