Une technique pour calculer la forme normale d'un terme en interprétant le terme dans un modèle sémantique approprié (évaluation) puis en réifiant ou lisant la valeur sémantique dans une forme syntaxique normale.

Principe

Évaluer des termes syntaxiques dans un domaine sémantique où les réductions sont réalisées implicitement par le modèle, puis réifier les valeurs sémantiques en syntaxe pour obtenir un représentant normal ou canonique.

Démonstration

Pour le λ-calcul simplement typé, interpréter les termes dans un modèle de fonctions et de termes neutres ; l'évaluation de (λx. M) N donne le résultat sémantique et la réification produit la forme β-normale, η-longue sans effectuer explicitement des β-réductions syntaxiques.

Mauvaise application

Utiliser un domaine sémantique qui ne respecte pas les congruences opérationnelles (par exemple ignorer les termes neutres) ou ne pas implémenter correctement la réification conduit à des formes normales incorrectes ou incomplètes.

Conséquence

La NbE conduit souvent à des algorithmes de normalisation efficaces, gère proprement les égalités extensionnelles (lois η) et sépare le contenu computationnel (évaluation) de la reconstruction syntaxique (réification), facilitant les preuves de normalisation et la décidabilité de l'égalité.

Inversion

La réciproque est la normalisation purement syntaxique par réécritures locales répétées (β-réduction, η-expansion) qui peut être moins modulaire et plus difficile à rattacher à des modèles computationnels.

Limite

S'applique lorsque l'on dispose d'une interprétation sémantique fidèle et d'une procédure de réification effective ; elle n'est pas applicable si la sémantique n'est pas calculable ou si la réification ne peut produire des représentants syntaxiques finis.

Tension sémantique

Tension entre construire des domaines sémantiques riches qui simplifient l'évaluation et conserver une réification faisable ; des modèles plus expressifs simplifient l'évaluation mais compliquent la réification en syntaxe.

Synthèse

La normalisation par évaluation calcule des formes syntaxiques canoniques en déléguant la réduction à un modèle sémantique puis en reconstruisant systématiquement la syntaxe, produisant une normalisation modulaire, souvent efficace et sémantiquement motivée.