domingo, 6 de junio de 2010

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)

 

0 comentarios:

Publicar un comentario