Sistema abstracte de reescriptura

En lògica matemàtica i informàtica teòrica, un sistema abstracte de reescriptura és un formalisme que captura les nocions essencials i les propietats dels sistemes de reescriptura. En la seva forma més simple, un sistema abstracte de reescriptura és un conjunt (d'"objectes") juntament amb una relació binària, que hom acostuma a denotar per $\rightarrow$ ; aquesta definició es pot refinar si s'indexen (és a dir, si s'etiqueten) els subconjunts de la relació binària. Tot i la seva simplicitat, un sistema abstracte de reescriptura és suficient per descriure algunes propietats importants dels sistemes de reescriptura, com per exemple les formes normals, la terminació i diverses nocions de confluència.

Històricament hi ha hagut diverses formalitzacions de la reescriptura en un context abstracte, cadascuna amb les seves característiques. Això és degut al fet que algunes nocions són equivalents. La formalització més comuna es deu a Gérard Huet (1980).^[1]

Definició

Un sistema abstracte de reescriptura és un conjunt A, els elements del qual hom acostuma a dir objectes, juntament amb una relació binària sobre A, notada habitualment per →, i anomenada relació de reducció, relació de reescriptura^[2] o simplement reducció.^[3] Aquesta terminologia pot resultar una mica confusa, ja que, encara que es parla de "reducció", la relació binària no té per què reduir necessàriament la mesura dels objectes.

En alguns contextos, pot ser útil distingir entre alguns subconjunts de regles, és a dir, alguns subconjunts de la relació de reducció →; per exemple, la relació pot consistir en regles d'associativitat i de commutativitat. Així, alguns autors defineixen la relació de reducció → com la unió indexada d'algunes relacions. Per exemple, si $\rightarrow _{1}\cup \rightarrow _{2}=\rightarrow$ , hom usa la notació (A, →₁, →₂).

Com a objecte matemàtic, un sistema abstracte de reescriptura és exactament el mateix que un sistema de transició d'estats sense etiquetar, i si hom considera la relació com una unió indexada, llavors un sistema abstracte de reescriptura és equivalent a un sistema de transició d'estats on els índexs són les etiquetes. L'objecte d'estudi, però, és diferent. En un sistema de transició d'estats, hom estudia les accions definides per les etiquetes, mentre que en un sistema abstracte de reescriptura s'estudia com es poden transformar (reescriure) els objectes.^[4]

Exemple

Suposem que el conjunt d'objectes és T = {a, b, c}, i que la relació binària ve donada per les regles a → b, b → a, a → c, i b → c. Observem que aquestes regles es poden aplicar tant a a com a b per obtenir c. Notem també que, en un cert sentit, c és l'objecte més "simple" del sistema, ja que no es pot aplicar cap regla per transformar c en cap altre objecte. Aquesta és una propietat important.

Nocions bàsiques

L'exemple anterior serveix de motivació per definir alguns conceptes bàsics sobre els sistemes abstractes de reescriptura:^[5]

${\stackrel {*}{\rightarrow }}$ és la clausura transitiva de $\rightarrow \cup =$ , on = és la relació d'igualtat, és a dir, ${\stackrel {*}{\rightarrow }}$ és el preordre més petit (això és, la relació reflexiva i transitiva més petita) que conté $\rightarrow$ . Hom diu també que és la clausura transitiva reflexiva de $\rightarrow$ .
$\leftrightarrow$ és $\rightarrow \cup \rightarrow ^{-1}$ , això és, la unió de la relació → amb la seva relació inversa, també coneguda com la clausura simètrica de $\rightarrow$ .
${\stackrel {*}{\leftrightarrow }}$ és la clausura transitiva de $\leftrightarrow \cup =$ , és a dir, ${\stackrel {*}{\leftrightarrow }}$ és la relació d'equivalència més petita que conté $\rightarrow$ . També es coneix com clausura simètrica transitiva reflexiva de $\rightarrow$ .

Formes normals i el problema de la paraula

Un objecte x d'A s'anomena reductible si existeix un altre y d'A tal que $x\rightarrow y$ ; si no existeix cap y així, hom diu que x és irreductible o que és una forma normal. Es diu que un objecte y és una forma normal de x si $x{\stackrel {*}{\rightarrow }}y$ , i y és irreductible. Si x té una forma normal única, s'acostuma a denotar $x\!\!\downarrow$ . En l'exemple anterior, c és una forma normal, i $c=a\!\!\downarrow \,=\,b\!\!\downarrow$ . Si tot objecte té almenys una forma normal, llavors es diu que el sistema abstracte de reescriptura és normalitzant.

Un dels problemes importants que es poden formular en un sistema abstracte de reescriptura és el problema de la paraula: donats x i y, hom pot preguntar-se si són equivalents segons ${\stackrel {*}{\leftrightarrow }}$ . Aquest és un plantejament general per a la formulació del problema de la paraula en una estructura algebraica. Per exemple, el problema de la paraula per a grups és un cas particular del problema de la paraula en un sistema abstracte de reescriptura. En tot cas, una solució "senzilla" per a aquest problema passa per l'existència de formes normals úniques: en tal cas, si dos objectes tenen la mateixa forma normal, llavors són equivalents segons ${\stackrel {*}{\leftrightarrow }}$ . El problema de la paraula per a un sistema abstracte de reescriptura és, en general, indecidible.

Unibilitat i la propietat de Church-Rosser

Una noció relacionada amb l'existència de formes normals, encara que més feble, és la de si dos objectes són unibles: hom diu que x i y són unibles si existeix algun z tal que $x{\stackrel {*}{\rightarrow }}z{\stackrel {*}{\leftarrow }}y$ . A partir d'aquesta definició, sembla natural definir la relació d'unibilitat com ${\stackrel {*}{\rightarrow }}\circ {\stackrel {*}{\leftarrow }}$ , on $\circ$ és la composició de relacions. La unibilitat es denota habitualment, d'una forma una mica confusa, amb el símbol $\downarrow$ , però en aquesta notació la fletxa cap avall és un operador binari, és a dir, hom escriu $x{\mathbin {\downarrow }}y$ si x i y són unibles.

Es diu que un sistema abstracte de reescriptura compleix la propietat de Church-Rosser si i només si $x{\stackrel {*}{\leftrightarrow }}y$ implica que $x{\mathbin {\downarrow }}y$ per a objectes qualssevol x, y. Equivalentment, la propietat de Church-Rosser significa que la clausura simètrica transitiva reflexiva està inclosa en la relació d'unibilitat. Alonzo Church i John Barkley Rosser van demostrar el 1936 que el càlcul lambda té aquesta propietat;^[6] d'aquí el nom de la propietat.^[7] (El fet que el càlcul lambda tingui aquesta propietat es coneix també com Teorema de Church-Rosser.) En un sistema abstracte de reescriptura que compleixi la propietat de Church-Rosser, hom pot reduir el problema de la paraula a la cerca d'un successor comú. En un sistema de Church-Rosser, un objecte té, com a màxim, una forma normal; és a dir, la forma normal d'un objecte, si existeix, és única, però pot no existir. Per exemple, en càlcul lambda, l'expressió (λx.xx)(λx.xx) no té una forma normal, perquè existeix una successió infinita de reduccions beta (λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ...^[8]

Nocions de confluència

Existeixen diverses propietats equivalents a Church-Rosser, i que tenen un enunciat més simple. Això ens permet demostrar que un sistema és Church-Rosser amb menys esforç. Addicionalment, hom pot definir les nocions de confluència com a propietats d'un objecte particular, cosa que no és possible si hom fa servir directament la definició de Church-Rosser.

Es diu que un sistema abstracte de reescriptura $(A,\rightarrow )$ és:

confluent si i només si per a qualssevol w, x i y d'A, $x{\stackrel {*}{\leftarrow }}w{\stackrel {*}{\rightarrow }}y$ implica $x{\mathbin {\downarrow }}y$ . En altres paraules, la confluència significa que no importa com són de diferents dos "camins" amb un ancestre comú (w), ja que els camins es troben en algun successor comú. Aquesta noció es pot refinar per tal de definir-la com a propietat d'un objecte particular w, i hom diu que un sistema és confluent si tots els seus elements ho són.
semiconfluent si i només si per a qualssevol w, x i y d'A, $x\leftarrow w{\stackrel {*}{\rightarrow }}y$ implica $x{\mathbin {\downarrow }}y$ . Aquesta propietat es diferencia de la confluència en la reducció en un sol pas de w a x.
localment confluent si i només si per a qualssevol w, x i y d'A, $x\leftarrow w\rightarrow y$ implica $x{\mathbin {\downarrow }}y$ . De vegades hom anomena a aquesta propietat confluència feble.

Teorema: En un sistema abstracte de reescriptura, les tres condicions següents són equivalents:

té la propietat de Church-Rosser
és confluent
és semi-confluent.^[9]

Corol·lari:^[10] En un sistema abstracte de reescriptura confluent, si $x{\stackrel {*}{\leftrightarrow }}y$ llavors

Si x i y són formes normals, llavors x = y.
Si y és una forma normal, llavors $x{\stackrel {*}{\rightarrow }}y$

Aquestes equivalències motiven lleugeres variacions en la bibliografia sobre les definicions. Per exemple, a Terese, es defineix la confluència com hem vist, i es presenta com sinònima de la propietat de Church-Rosser.^[11] Arran del corol·lari anterior, hom pot definir una forma normal y d'x com un y irreductible tal que $x{\stackrel {*}{\leftrightarrow }}y$ . Aquesta definició, que es pot trobar a Book & Otto 1993, és equivalent a la que hem vist anteriorment per a un sistema confluent, però és més inclusiva si es parla d'un sistema abstracte de reescriptura no confluent.

D'altra banda, la confluència local no és equivalent a altres nocions de confluència que hem vist, sinó que és estrictament més feble que la confluència. El contraexemple típic és $\{a\rightarrow b,b\rightarrow a,a\rightarrow x,b\rightarrow y\}$ , que és localment confluent, però no confluent.

Terminació i convergència

Hom diu que un sistema abstracte de reescriptura és terminant o noetherià si no existeix cap cadena infinita $x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots$ (això és equivalent a dir que la relació de reescriptura és una relació noetheriana.) En un sistema abstracte de reescriptura noetherià, tot objecte té almenys una forma normal, i per tant és normalitzant. El recíproc no és pas cert, en general: per exemple, a l'exemple anterior, existeix una cadena infinita ( $a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots$ ), encara que el sistema és normalitzant. Si un sistema abstracte de reescriptura és confluent i noetherià, hom diu que el sistema és canònic^[12] o convergent. En un sistema abstracte de reescriptura convergent, tot objecte té una única forma normal; però n'hi ha prou amb què el sistema sigui confluent i normalitzant per tal que existeixi una forma normal única per a cada element, com s'ha vist a l'exemple.

Teorema (Lema de Newman): Un sistema abstracte de reescriptura terminant és confluent si i només si és localment confluent.

La demostració original de Newman de l'any 1942 és força complicada. El 1980, Huet publicà una altra demostració que explotava el fet que quan $\rightarrow$ és terminant, hom pot aplicar inducció ben fonamentada.^[13]

Referències

↑ Book i Otto, 1993, p. 9.
↑ Bezem, Klop i de Vrijer, 2003, p. 7.
↑ Book i Otto, 1993, p. 10.
↑ Bezem, Klop i de Vrijer, 2003, p. 7-8.
↑ Baader i Nipkow, 1998, p. 8-9.
↑ Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936
↑ Baader i Nipkow, 1998, p. 9.
↑ Cooper, S. Barry. Computability theory. Chapman and Hall/CRC, 17 novembre 2003, p. 184. ISBN 978-1584882374.
↑ Baader i Nipkow, 1998, p. 11.
↑ Baader i Nipkow, 1998, p. 12.
↑ Bezem, Klop i de Vrijer, 2003, p. 11.
↑ Duffy, David A. «secció 7.2.1». A: Principles of Automated Theorem Proving. Wiley, 1991, p. 153.
↑ Harrison, John. «chapter 4 "Equality"». A: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009, p. 260. ISBN 978-0-521-89957-4.

Bibliografia

Baader, Franz; Nipkow, Tobias. Term Rewriting and All That. Cambridge University Press, 1998.
Nachum Dershowitz and Jean-Pierre Jouannaud Rewrite Systems, Chapter 6 in Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics., Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, pp. 243–320. The preprint of this chapter is freely available from the authors, but it misses the figures.
Book, Ronald V.; Otto, Friedrich. «Chapter 1, "Abstract reduction systems"». A: String-rewriting Systems. Springer, 1993.
Bezem, Marc; Klop, Jan Willem; de Vrijer, Roel. «Chapter 1». A: Term rewriting systems ("Terese"). Cambridge University Press, 2003. ISBN 0-521-39115-6.
Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797–821. Huet's paper established many of the modern concepts, results and notations.
Sinyor, J.; "The 3x+1 Problem as a String Rewriting System", International Journal of Mathematics and Mathematical Sciences, Volume 2010 (2010), Article ID 458563, 6 pages.

[FOOTNOTEBookOtto19939-1] Book i Otto, 1993, p. 9.

[FOOTNOTEBezemKlopde_Vrijer20037-2] Bezem, Klop i de Vrijer, 2003, p. 7.

[FOOTNOTEBookOtto199310-3] Book i Otto, 1993, p. 10.

[FOOTNOTEBezemKlopde_Vrijer20037-8-4] Bezem, Klop i de Vrijer, 2003, p. 7-8.

[FOOTNOTEBaaderNipkow19988-9-5] Baader i Nipkow, 1998, p. 8-9.

[6] Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936

[FOOTNOTEBaaderNipkow19989-7] Baader i Nipkow, 1998, p. 9.

[8] Cooper, S. Barry. Computability theory. Chapman and Hall/CRC, 17 novembre 2003, p. 184. ISBN 978-1584882374.

[FOOTNOTEBaaderNipkow199811-9] Baader i Nipkow, 1998, p. 11.

[FOOTNOTEBaaderNipkow199812-10] Baader i Nipkow, 1998, p. 12.

[FOOTNOTEBezemKlopde_Vrijer200311-11] Bezem, Klop i de Vrijer, 2003, p. 11.

[12] Duffy, David A. «secció 7.2.1». A: Principles of Automated Theorem Proving. Wiley, 1991, p. 153.

[13] Harrison, John. «chapter 4 "Equality"». A: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009, p. 260. ISBN 978-0-521-89957-4.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]