En reescritura abstracta , [1] un objeto está en forma normal si no puede reescribirse 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.
Dicho formalmente, si ( A ,→) es un sistema de reescritura abstracto , x ∈ A está en forma normal si no existe y ∈ A tal que x → y , es decir, x es un término irreducible.
Un objeto a se normaliza débilmente si existe al menos una secuencia particular de reescrituras a partir de a que eventualmente produce una forma normal. Un sistema de reescritura tiene la propiedad de normalización débil o se está normalizando (débilmente) (WN) si cada objeto se está normalizando débilmente. Un objeto a se normaliza fuertemente si cada secuencia de reescrituras que comienza desde a eventualmente termina con una forma normal. Un sistema de reescritura abstracta es fuertemente normalizante , terminante , noetheriano o tiene la propiedad de normalización (fuerte) (SN), si cada uno de sus objetos está fuertemente normalizado. [2]
Un sistema de reescritura tiene la propiedad de forma normal (NF) si para todos los objetos a y formas normales b , se puede llegar a b 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 , se puede llegar a 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 la 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]
Esta sección presenta algunos resultados bien conocidos. Primero, SN implica WN. [4]
Confluencia (abreviado CR) implica NF implica ONU implica ONU → . [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 un reducto común.
WN y ONU → implican confluencia. Por 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 destacable 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 normalizadores (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 de normalización ya que desde cualquier término, por ejemplo, r (4,2) comienza una única secuencia de reescritura, verbigracia. r (4,2) → r (2,4) → r (4,2 ) → r (2,4) → ..., que es infinitamente largo. Esto lleva a la idea de reescribir el "módulo de conmutatividad ", donde un término está en forma normal si no se aplican otras reglas que la conmutatividad. [8]
El sistema { b → a , b → c , c → b , c → d } (en la foto) es un ejemplo de un sistema que se normaliza débilmente pero no se normaliza fuertemente. 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, y ni siquiera la propiedad de normalización débil. Considere el término (la aplicación es asociativa izquierda ). Tiene la siguiente regla de reescritura: Para cualquier término ,
Pero considere lo que sucede cuando lo aplicamos a sí mismo:
Por lo tanto, el término no es fuertemente normalizador. Y esta es la única secuencia de reducción, por lo que tampoco es una normalización débil.
Varios sistemas de cálculo lambda tipificado , incluido el cálculo lambda tipificado simplemente , el Sistema F de Jean-Yves Girard y el cálculo de construcciones de Thierry Coquand , se están normalizando fuertemente.
Un sistema de cálculo lambda con la propiedad de normalización puede verse 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 detención viendo si el tipo de programa verifica. Esto significa que hay funciones computables que no se pueden definir en el cálculo lambda simplemente tipado, 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]
