La propriété d’un système de réduction (réécriture ou calcul) selon laquelle toute suite de réductions possible, partant de n’importe quel terme, est finie ; en d’autres termes, aucun terme n’admet de chaîne infinie de réductions et chaque terme atteint donc une forme normale.

Principe

La relation de réduction est bien fondée : il n’existe pas de chaîne infinie t0 → t1 → t2 → … ; par conséquent toute suite de réductions doit s’arrêter sur une forme qui n’admet plus de règle applicable.

Démonstration

Dans le lambda-calcul simplement typé, on établit la normalisation forte en construisant des relations logiques ou des candidats de réductibilité qui montrent qu’un terme typé ne peut pas admettre une suite infinie de β-réductions, et aboutit donc à une forme normale.

Mauvaise application

Prétendre que le lambda-calcul non typé ou un système autorisant la récursion générale est normalisant fort ; ou confondre normalisation forte avec normalisation faible ou avec une terminaison dépendant d’une stratégie particulière de réduction.

Conséquence

Les programmes correspondant aux termes dans un système normalisant fort terminent toujours ; la normalisation forte combinée à la confluence permet la décidabilité de la convertibilité et sert aux preuves de consistance des théories de types.

Inversion

La négation de la normalisation forte est l’existence d’au moins un terme admettant des suites de réductions infinies (divergence) ; dans ce cas il existe des calculs qui n’atteignent jamais de forme normale.

Limite

S’applique aux relations de réduction abstraites et aux calculs sans effets de bord ; elle ne s’étend pas directement aux systèmes contenant des primitivess non terminantes (récursion générale, boucles d’E/S) et ne doit pas être confondue avec la normalisation faible qui n’exige qu’un chemin terminal.

Tension sémantique

Tension avec la normalisation faible (qui demande seulement l’existence d’un chemin terminé) et avec la confluence (qui porte sur l’unicité des formes normales) : un système peut être confluent sans être normalisant fort, ou normalisant fort sans être confluent dans des définitions pathologiques.

Synthèse

La normalisation forte est la garantie globale de terminaison pour un système de réécriture : elle affirme qu’aucun terme n’autorise de descente infinie selon les règles de réduction et qu’il atteint donc toujours une forme normale, facilitant l’extraction de résultats canoniques et les arguments de consistance.