Die Eigenschaft eines Reduktionssystems (Umschreibungs- oder Berechnungskalküls), dass jede mögliche Reduktionsfolge von jedem Term aus endlich ist; mit anderen Worten besitzt kein Term eine unendliche absteigende Folge von Reduktionen, und jeder Term erreicht eine Normalform.

Prinzip

Wohlbegründetheit der Reduktionsrelation: Es existiert keine unendliche Kette t0 → t1 → t2 → …, daher muss jede Reduktionsfolge in einer nicht weiter reduzierbaren Form enden.

Demonstration

Im einfach getypten Lambda-Kalkül beweist man starke Normalisierung mittels logischer Relationen oder der Methode der Reduzibilitätskandidaten, sodass jeder getypte Term keine unendliche β-Reduktionsfolge haben kann und folglich eine Normalform besitzt.

Fehlanwendung

Davon auszugehen, dass das ungetypte Lambda-Kalkül oder ein System mit uneingeschränkter Rekursion starke Normalisierung besitzt; oder starke Normalisierung mit schwacher Normalisierung bzw. mit Strategienspezifischer Terminierung zu verwechseln.

Konsequenz

Programme, die Termen in einem stark normalisierenden System entsprechen, terminieren stets; starke Normalisierung zusammen mit Konfluenz ermöglicht die Entscheibarkeit der Konvertierbarkeit und stützt Konsistenzbeweise für Typentheorien.

Umkehrung

Die Verneinung starker Normalisierung ist die Existenz wenigstens eines Terms mit unendlicher Reduktionsfolge (Divergenz); in solchen Systemen existieren Berechnungen, die niemals eine Normalform erreichen.

Abgrenzung

Gilt für abstrakte Reduktionsrelationen und Kalküle ohne Seiteneffekte; deckt keine Systeme mit nicht-terminierenden Primitiven (allgemeine Rekursion, I/O-Schleifen) ab und ist nicht mit schwacher Normalisierung gleichzusetzen, die nur die Existenz eines terminierenden Pfads fordert.

Semantische Spannung

Spannung gegenüber schwacher Normalisierung (nur ein terminierender Pfad nötig) und gegenüber Konfluenz (Eindeutigkeit der Normalformen): Ein System kann konvergent, aber nicht stark normalisierend sein, oder stark normalisierend, aber in pathologischen Fällen nicht konvergent.

Synthese

Starke Normalisierung ist die universelle Terminierungseigenschaft eines Rewriting- oder Berechnungssystems: sie garantiert, dass kein Term unendlich nach unten reduziert werden kann und daher alle Terme eine Normalform erreichen, was kanonische Resultate und Konsistenzargumente ermöglicht.