Forma normal (reescritura abstracta)

En la 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.

Definiciones

Dicho 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 normalizador si existe al menos una secuencia particular de reescrituras que parte de a y que finalmente produce una forma normal. Un sistema de reescritura tiene la propiedad de normalización débil o es (débilmente) normalizador (WN) si cada objeto es débilmente normalizador. Un objeto a es fuertemente normalizador si cada secuencia de reescrituras que parte de a termina finalmente con una forma normal. Un sistema de reescritura es fuertemente normalizador , terminante , noetheriano o tiene la propiedad de normalización (fuerte) (SN), si cada uno de sus objetos es fuertemente normalizador. ^{[ 2 ]}

Un sistema de reescritura tiene la propiedad de forma normal (FN) 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 de forma normal única (UN) si para todas las formas normales a , b ∈ S , se puede llegar a 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 de forma normal única 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 ]}

Resultados

Esta sección presenta algunos resultados bien conocidos. Primero, SN implica WN. ^{[ 4 ]}

Confluencia (abreviado 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 reducto común.

WN y UN ^→ implican confluencia. Por lo tanto, CR, NF, UN y UN ^→ coinciden si WN es cierto. ^{[ 5 ]}

Ejemplos

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 ]}

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24

(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

Ejemplos de sistemas no normalizadores (ni débil ni fuertemente) incluyen el conteo 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 desde cualquier término, por ejemplo r (4,2) comienza una única secuencia de reescritura, a saber, r (4,2) → r (2,4) → r (4,2) → r (2,4) → ..., que es infinitamente larga. Esto lleva a la idea de reescribir "módulo conmutatividad " donde un término está en forma normal si no se aplican más reglas que la conmutatividad. ^[⁸^]

El sistema { b → a , b → c , c → b , c → d } (en la imagen) es un ejemplo de un sistema débilmente normalizador pero no fuertemente normalizador. a y d son formas normales, y b y c se pueden reducir a a o d , pero la reducción infinita b → c → b → c → ... significa que ni b ni c son fuertemente normalizadores.

cálculo lambda sin tipado

El cálculo lambda puro no tipado no satisface la propiedad de normalización fuerte, ni siquiera la propiedad de normalización débil. Consideremos el término $\lambda x.xxx$ (la aplicación es asociativa por la izquierda ). Tiene la siguiente regla de reescritura: Para cualquier término $t$ ,

(\mathbf {\lambda } x.xxx)t\rightarrow ttt

Pero consideremos qué sucede cuando aplicamos $\lambda x.xxx$ a sí mismo:

{\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \cdots \,\end{aligned}}

Por lo tanto, el término $(\lambda x.xxx)(\lambda x.xxx)$ no es fuertemente normalizador. Y esta es la única secuencia de reducción, por lo tanto, tampoco es débilmente normalizador.

cálculo lambda tipado

Diversos sistemas de cálculo lambda tipado, entre los que se incluyen el cálculo lambda tipado simple , 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 considerarse un lenguaje de programación con la propiedad de que todo programa termina . Si bien 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 , ya que de lo contrario se podría resolver el problema de la parada comprobando si el tipo del programa es correcto. Esto significa que existen funciones computables que no pueden definirse en el cálculo lambda de tipado simple, y lo mismo ocurre con 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 ]}

Véase también

Referencias

↑ Franz Baader ; Tobias Nipkow (1998). Term Rewriting and All That . Cambridge University Press . ISBN 9780521779203.
↑ Ohlebusch, Enno (1998). "Teoremas de Church-Rosser para la reducción abstracta módulo una relación de equivalencia" . Técnicas y aplicaciones de reescritura . Notas de clase en informática. Vol. 1379. p. 18. doi : 10.1007/BFb0052358 . ISBN 978-3-540-64301-2.
1 2 Klop, JW; de Vrijer, RC (febrero de 1989). "Formas normales únicas para el cálculo lambda con emparejamiento sobreyectivo" . Information and Computation . 80 (2): 97– 113. doi : 10.1016/0890-5401(89)90014-X .
↑ "lógica - ¿Cuál es la diferencia entre la normalización fuerte y la normalización débil en el contexto de los sistemas de reescritura?" . Computer Science Stack Exchange . Consultado el 12 de septiembre de 2021 .
↑ Ohlebusch, Enno (17 de abril de 2013). Temas avanzados en la reescritura de términos . Springer Science & Business Media. págs. 13–14 . ISBN 978-1-4757-3661-8.
↑ Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. pág. 1. ISBN 0-521-39115-6.
↑ Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. pág. 2. ISBN 0-521-39115-6.
↑ Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). "6. Reescribir sistemas". En Jan van Leeuwen (ed.). Manual de informática teórica . vol. B. Elsevier. págs. 9– 10. CiteSeerX 10.1.1.64.3114 . ISBN 0-444-88074-7.
↑ N. Dershowitz y J.-P. Jouannaud (1990). «Sistemas de reescritura». En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. pág. 268. ISBN 0-444-88074-7.
↑ Riolo, Rick; Worzel, William P.; Kotanchek, Mark (4 de junio de 2015). Teoría y práctica de la programación genética XII . Springer. pág. 59. ISBN 978-3-319-16030-6. Consultado el 8 de septiembre de 2021 .

[1] Franz Baader ; Tobias Nipkow (1998). Term Rewriting and All That . Cambridge University Press . ISBN 9780521779203.

[2] Ohlebusch, Enno (1998). "Teoremas de Church-Rosser para la reducción abstracta módulo una relación de equivalencia" . Técnicas y aplicaciones de reescritura . Notas de clase en informática. Vol. 1379. p. 18. doi : 10.1007/BFb0052358 . ISBN 978-3-540-64301-2.

[NF-3] 1 2 Klop, JW; de Vrijer, RC (febrero de 1989). "Formas normales únicas para el cálculo lambda con emparejamiento sobreyectivo" . Information and Computation . 80 (2): 97– 113. doi : 10.1016/0890-5401(89)90014-X .

[4] "lógica - ¿Cuál es la diferencia entre la normalización fuerte y la normalización débil en el contexto de los sistemas de reescritura?" . Computer Science Stack Exchange . Consultado el 12 de septiembre de 2021 .

[5] Ohlebusch, Enno (17 de abril de 2013). Temas avanzados en la reescritura de términos . Springer Science & Business Media. págs. 13–14 . ISBN 978-1-4757-3661-8.

[6] Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. pág. 1. ISBN 0-521-39115-6.

[7] Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. pág. 2. ISBN 0-521-39115-6.

[8] Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). "6. Reescribir sistemas". En Jan van Leeuwen (ed.). Manual de informática teórica . vol. B. Elsevier. págs. 9– 10. CiteSeerX 10.1.1.64.3114 . ISBN 0-444-88074-7.

[Dershowitz.Jouannaud.1990.Fig2-9] N. Dershowitz y J.-P. Jouannaud (1990). «Sistemas de reescritura». En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol. B. Elsevier. pág. 268. ISBN 0-444-88074-7.

[10] Riolo, Rick; Worzel, William P.; Kotanchek, Mark (4 de junio de 2015). Teoría y práctica de la programación genética XII . Springer. pág. 59. ISBN 978-3-319-16030-6. Consultado el 8 de septiembre de 2021 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[

[ 9 ]

[ 10 ]