La propiedad de un sistema de reducción (reescritura o cálculo) según la cual toda secuencia de reducción posible que parte de cualquier término es finita; equivalentemente, ningún término admite una cadena infinita de reducciones y por tanto alcanza una forma normal.

Principio

La relación de reducción es bien fundada: no existe una cadena infinita t0 → t1 → t2 → …, de modo que toda secuencia de reducción debe terminar en una forma que ya no admite reglas aplicables.

Demostración

En el cálculo lambda simplemente tipado se prueba la normalización fuerte mediante relaciones lógicas o candidatos de reducibilidad, demostrando que todo término tipado carece de una secuencia infinita de β-reducciones y por tanto llega a una forma normal.

Aplicación incorrecta

Suponer que el cálculo lambda no tipado o un sistema con recursión general es normalizante fuerte; o confundir normalización fuerte con normalización débil o con terminación dependiente de una estrategia concreta de reducción.

Consecuencia

Los programas correspondientes a términos en un sistema con normalización fuerte siempre terminan; la normalización fuerte junto con la confluencia conduce a decisibilidad de convertibilidad y apoya pruebas de consistencia en teorías de tipos.

Inversión

La negación de la normalización fuerte es la existencia de al menos un término con secuencias de reducción infinitas (divergencia); en estos sistemas existen cómputos que nunca alcanzan una forma normal.

Límite

Se aplica a relaciones de reducción abstractas y cálculos sin efectos secundarios; no cubre directamente sistemas con primitivas no terminantes (recursión general, bucles de E/S) y no es equivalente a la normalización débil, que solo exige la existencia de algún camino que termine.

Tensión semántica

Tensión con la normalización débil (que requiere solo un camino terminante) y con la confluencia (que trata la unicidad de las formas normales): un sistema puede ser confluyente sin ser fuertemente normalizante, o fuertemente normalizante sin ser confluyente en definiciones patológicas.

Síntesis

La normalización fuerte es la garantía global de terminación para un sistema de reescritura o cálculo: afirma que ningún término permite una caída infinita según las reglas de reducción y que por tanto todos los términos alcanzan una forma normal, posibilitando extracción de resultados canónicos y razonamientos de consistencia.