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 byc, y b,c no tienen un reducto común.
WN y ONU → 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 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]
