Formas normales

He descubierto un artículo donde aparecen muy bien explicadas las distintas formas normales del lambda cálculo. El artículo es este y se resume en la siguiente tabla:

	Reduce bajo abstracciones	No reduce bajo abstracciones
Reduce argumentos	v ::= λx.v | x v1 … vn Forma normal (NF)	v ::= λx.e | x v1 … vn Forma normal débil (WNF)
No reduce argumentos	v ::= λx.v | x e1 … en Forma normal de cabeza (HNF)	v ::= λx.e | x e1 … en Forma normal débil de cabeza (WHNF)

He puesto entre paréntesis las iniciales de las formas normales en inglés (Normal Form, Weak Normal Form, Head Normal Form y Weak Head Normal Form).

El grupo sintáctico v es el de los términos que se consideran forma normal. El grupo sintáctico e es el de los términos del lambda cálculo. Éstos se definen así:

e ::= x | λx.e | e1 e2

Estas formas normales se usan luego para definir las propiedades de los términos. Por ejemplo, un término fuertemente normalizable (SF) es un término que, usemos la estrategia de evaluación que usemos, siempre alcanza una forma normal (NF).

Un término tiene forma normal si existe una estrategia de evaluación que llegue a esa forma normal. De hecho, las estrategias de evaluación están enfocadas a llegar a una forma normal en concreto. Las estrategias que siempre llegan a esa forma normal deseada se denominan estrategias normalizantes.

La siguiente tabla define las estrategias de evaluación más usuales según reduzcan los términos exteriores o interiores primero.

Forma normal deseada	Primero términos exteriores	Primero términos interiores
NF	Orden normal (Normalizante)	Orden aplicativo (No normalizante)
WNF		Llamada por valor (No normalizante)
WHNF	Llamada por nombre (Normalizante)