En la reescritura abstracta , [1] un objeto está en forma normal si no se puede reescribir más, es decir, es irreducible. Dependiendo del sistema de reescritura, un objeto puede reescribirse en varias formas normales o en ninguna. Muchas propiedades de los sistemas de reescritura se relacionan con las formas normales.
Enunciado formalmente, si ( A ,→) es un sistema de reescritura abstracto , x ∈ A está en forma normal si no existe ningún y ∈ A tal que x → y , es decir, x es un término irreducible.
Un objeto a es débilmente normalizante si existe al menos una secuencia particular de reescrituras que comienzan desde a y que finalmente dan lugar a una forma normal. Un sistema de reescritura tiene la propiedad de normalización débil o es (débilmente) normalizante (WN) si cada objeto es débilmente normalizante. Un objeto a es fuertemente normalizante si cada secuencia de reescrituras que comienzan desde a finalmente termina con una forma normal. Un sistema de reescritura abstracto es fuertemente normalizante , terminal , noetheriano o tiene la propiedad de normalización (fuerte) (SN), si cada uno de sus objetos es fuertemente normalizante. [2]
Un sistema de reescritura tiene la propiedad de forma normal (NF) si para todos los objetos a y formas normales b , b puede alcanzarse desde a mediante una serie de reescrituras y reescrituras inversas solo si a se reduce a b . Un sistema de reescritura tiene la propiedad única de forma normal (UN) si para todas las formas normales a , b ∈ S , a puede alcanzarse desde b mediante una serie de reescrituras y reescrituras inversas solo si a es igual a b . Un sistema de reescritura tiene la propiedad única de forma normal con respecto a la reducción (UN → ) si para cada término que se reduce a las formas normales a y b , a es igual a b . [3]
En esta sección se presentan algunos resultados conocidos. En primer lugar, SN implica WN. [4]
La confluencia (abreviada CR) implica NF implica UN implica UN → . [3] Las implicaciones inversas generalmente no se cumplen. {a→b,a→c,c→c,d→c,d→e} es UN → pero no UN ya que b=e y b,e son formas normales. {a→b,a→c,b→b} es UN pero no NF ya que b=c, c es una forma normal y b no se reduce a c. {a→b,a→c,b→b,c→c} es NF ya que no hay formas normales, pero no CR ya que a se reduce a b y c, y b,c no tienen una reducción común.
WN y UN → implican confluencia. Por lo tanto, CR, NF, UN y UN → coinciden si se cumple WN. [5]
Un ejemplo es que la simplificación de expresiones aritméticas produce un número (en aritmética, todos los números son formas normales). Un hecho notable es que todas las expresiones aritméticas tienen un valor único, por lo que el sistema de reescritura es fuertemente normalizador y confluente: [6]
Ejemplos de sistemas no normalizantes (ni débil ni fuertemente) incluyen contar hasta el infinito (1 ⇒ 2 ⇒ 3 ⇒ ...) y bucles como la función de transformación de la conjetura de Collatz (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., es un problema abierto si hay otros bucles de la transformación de Collatz). [7] Otro ejemplo es el sistema de regla única { r ( x , y ) → r ( y , x ) }, que no tiene propiedades normalizadoras ya que a partir de cualquier término, p. ej . r (4,2) comienza una secuencia de reescritura única, a saber, r (4,2) → r ( 2,4) → r (4,2) → r (2,4) → ..., que es infinitamente larga. Esto conduce a la idea de reescribir "módulo conmutatividad ", donde un término está en forma normal si no se aplican reglas distintas a la conmutatividad. [8]
El sistema { b → a , b → c , c → b , c → d } (en la imagen) es un ejemplo de un sistema débilmente normalizante pero no fuertemente normalizante. a y d son formas normales, y b y c pueden reducirse a a o d , pero la reducción infinita b → c → b → c → ... significa que ni b ni c son fuertemente normalizantes.
El cálculo lambda puro sin tipo no satisface la propiedad de normalización fuerte, ni siquiera la propiedad de normalización débil. Consideremos el término (la aplicación es asociativa por la izquierda ). Tiene la siguiente regla de reescritura: Para cualquier término ,
Pero consideremos lo que sucede cuando aplicamos a sí mismo:
Por lo tanto, el término no es fuertemente normalizante. Y esta es la única secuencia de reducción, por lo que tampoco es débilmente normalizante.
Varios sistemas de cálculo lambda tipificado , incluido el cálculo lambda simplemente tipificado , el sistema F de Jean-Yves Girard y el cálculo de construcciones de Thierry Coquand, son fuertemente normalizadores.
Un sistema de cálculo lambda con la propiedad de normalización puede ser visto como un lenguaje de programación con la propiedad de que cada programa termina . Aunque esta es una propiedad muy útil, tiene un inconveniente: un lenguaje de programación con la propiedad de normalización no puede ser Turing completo , de lo contrario, se podría resolver el problema de la detención viendo si el tipo de programa se verifica. Esto significa que hay funciones computables que no se pueden definir en el cálculo lambda de tipo simple, y de manera similar para el cálculo de construcciones y el Sistema F. Un ejemplo típico es el de un autointérprete en un lenguaje de programación total . [10]
