Eine Technik zur Berechnung der Normalform eines Terms, indem der Term in einem geeigneten semantischen Modell interpretiert (Auswertung) und dann der semantische Wert wieder in eine syntaktische Normalform reifiziert beziehungsweise zurückgelesen wird.

Prinzip

Syntaktische Terme in eine semantische Domäne auswerten, in der Reduktionen implizit durch das Modell erfolgen, und semantische Werte dann in die Syntax zurückreifizieren, um eine normale oder kanonische Repräsentante zu erhalten.

Demonstration

Für den einfach getypten λ-Kalkül Terme in einem Modell von Funktionen und neutralen Termen interpretieren; die Auswertung von (λx. M) N liefert das semantische Resultat und die Reifikation erzeugt die β-normale, η-lange Form ohne explizite syntaktische β-Schritte.

Fehlanwendung

Die Verwendung einer semantischen Domäne, die operationale Kongruenzen nicht respektiert (z. B. Ignorieren neutraler Terme) oder fehlerhafte Reifikation führt zu falschen oder unvollständigen Normalformen.

Konsequenz

NbE liefert oft effiziente Normalisierungsalgorithmen, behandelt extensionale Gleichheiten sauber (η-Gesetze) und trennt den rechnerischen Gehalt (Auswertung) von der syntaktischen Rekonstruktion (Reifikation), was Beweise der Normalisierung und Entscheidbarkeit von Gleichheit erleichtert.

Umkehrung

Die Umkehrung ist reine syntaktische Normalisierung durch wiederholte lokale Umschreibungsregeln (β-Reduktion, η-Expansion), die weniger modular sein kann und schwerer an Rechenmodelle anbindbar ist.

Abgrenzung

Gilt, wenn eine treue semantische Interpretation und ein effektives Reifikationsverfahren existieren; nicht anwendbar, wenn die Semantik nicht berechenbar ist oder Reifikation keine endlichen syntaktischen Repräsentanten erzeugen kann.

Semantische Spannung

Es besteht Spannung zwischen dem Aufbau reicher semantischer Domänen, die die Auswertung vereinfachen, und der Machbarkeit der Reifikation; ausdrucksvollere Modelle vereinfachen die Auswertung, erschweren jedoch die Rückübersetzung in Syntax.

Synthese

Normalisierung durch Auswertung berechnet kanonische syntaktische Formen, indem Reduktion an ein semantisches Modell delegiert und die Syntax systematisch rekonstruiert wird; dies ergibt eine modulare, oft effiziente Normalisierung mit klarer semantischer Rechtfertigung.