Una técnica para calcular la forma normal de un término interpretando el término en un modelo semántico adecuado (evaluación) y luego reificando o leyendo de nuevo el valor semántico a una forma sintáctica normal.

Principio

Evaluar términos sintácticos en un dominio semántico donde las reducciones se realizan implícitamente mediante el modelo, luego reificar los valores semánticos a sintaxis para obtener un representante normal o canónico.

Demostración

Para el cálculo λ simplemente tipado, interpretar términos en un modelo de funciones y términos neutrales; evaluar (λx. M) N produce el resultado semántico y la reificación genera la forma β-normal, η-larga sin efectuar pasos β sintácticos explícitos.

Aplicación incorrecta

Usar un dominio semántico que no respete las congruencias operacionales (por ejemplo ignorando términos neutrales) o implementar incorrectamente la reificación conduce a formas normales incorrectas o incompletas.

Consecuencia

NbE suele dar algoritmos de normalización eficientes, maneja bien igualdades extensionales (leyes η) y separa el contenido computacional (evaluación) de la reconstrucción sintáctica (reificación), facilitando pruebas de normalización y decidibilidad de igualdad.

Inversión

La inversión es la normalización puramente sintáctica por reescritura local repetida (β-reducción, η-expansión) que puede ser menos modular y más difícil de relacionar con modelos de computación.

Límite

Se aplica cuando existe una interpretación semántica fiel y un procedimiento de reificación efectivo; no es aplicable cuando la semántica no es computable o la reificación no puede producir representantes sintácticos finitos.

Tensión semántica

Hay tensión entre construir dominios semánticos ricos que simplifiquen la evaluación y mantener la reificación factible; modelos más expresivos facilitan la evaluación pero complican la reificación a la sintaxis.

Síntesis

La normalización por evaluación obtiene formas sintácticas canónicas delegando la reducción a un modelo semántico y reconstruyendo sistemáticamente la sintaxis, resultando en una normalización modular, a menudo eficiente y con justificación semántica clara.