##  [Starke Normalisierung](/de/node/60950) 

 Definition

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

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

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

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

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

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

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

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

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.