Mostra la font per a Sistema abstracte de reescriptura

En [[lògica matemàtica]] i [[informàtica teòrica]], un '''sistema abstracte de reescriptura''' és un [[Formalisme (matemàtiques)|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 <math>\rightarrow</math>; 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 [[Forma normal (reescriptura)|formes normals]], la [[Terminació (reescriptura)|terminació]] i diverses nocions de [[Confluència (reescriptura)|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).{{sfn|Book|Otto|1993|p=9}}

== 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'''{{sfn|Bezem|Klop|de Vrijer|2003|p=7|ref=Terese}} o simplement '''reducció'''.{{sfn|Book|Otto|1993|p=10}} 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'[[Propietat associativa|associativitat]] i de [[Propietat commutativa|commutativitat]]. Així, alguns autors defineixen la relació de reducció → com la unió indexada d'algunes relacions. Per exemple, si <math>\rightarrow_1 \cup \rightarrow_2 = \rightarrow</math>, hom usa la notació (''A'', →<sub>1</sub>, →₂).

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.{{sfn|Bezem|Klop|de Vrijer|2003|pp=7-8|ref=Terese}}

== 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|exemple]] anterior serveix de motivació per definir alguns conceptes bàsics sobre els sistemes abstractes de reescriptura:{{sfn|Baader|Nipkow|1998|pp=8-9}}
* <math>\stackrel{*}{\rightarrow}</math> és la ''[[clausura transitiva]]'' de <math>\rightarrow \cup =</math>, on = és la [[Igualtat (matemàtiques)|relació d'igualtat]], és a dir, <math>\stackrel{*}{\rightarrow}</math> és el [[preordre]] més petit (això és, la [[relació reflexiva]] i [[Relació transitiva|transitiva]] més petita) que conté <math>\rightarrow</math>. Hom diu també que és la ''clausura transitiva reflexiva'' de <math>\rightarrow</math>.
* <math>\leftrightarrow</math> és <math>\rightarrow \cup \rightarrow^{-1}</math>, això és, la unió de la relació → amb la seva [[relació inversa]], també coneguda com la ''[[clausura simètrica]]'' de <math>\rightarrow</math>.
* <math>\stackrel{*}{\leftrightarrow}</math> és la ''clausura transitiva'' de <math>\leftrightarrow \cup =</math>, és a dir, <math>\stackrel{*}{\leftrightarrow}</math> és la [[relació d'equivalència]] més petita que conté <math>\rightarrow</math>. També es coneix com ''clausura simètrica transitiva reflexiva'' de <math>\rightarrow</math>.

== Formes normals i el problema de la paraula ==
[[Fitxer:Solving the word problem without and with completion_svg.svg|miniatura|Resolució del problema de la paraula: el procés de decidir si <math>x \stackrel{*}{\leftrightarrow} y</math> requereix habitualment una cerca heurística ({{color|#c00000|vermell}}, {{color|#00c000|verd}}), mentre que decidir <math>x\!\!\downarrow \,= \,y\!\!\downarrow</math> és un procés senzill ({{color|#808080|gris}}). Per sistemes de reescriptura de termes, l'[[algorisme de Knuth-Bendix]] amplia <math>\rightarrow</math> per establir formes normals úniques, si és possible.]]
Un objecte ''x'' d{{'}}''A'' s'anomena '''reductible''' si existeix un altre ''y'' d{{'}}''A'' tal que <math>x \rightarrow y</math>; 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 <math>x \stackrel{*}{\rightarrow} y</math>, i ''y'' és irreductible. Si ''x'' té una forma normal ''única'', s'acostuma a denotar <math>x\!\!\downarrow</math>. En l'[[#Exemple|exemple]] anterior, ''c'' és una forma normal, i <math>c = a\!\!\downarrow \,= \,b\!\!\downarrow</math>. 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 <math>\stackrel{*}{\leftrightarrow}</math>. Aquest és un plantejament general per a la formulació del [[Problema de la paraula|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 <math>\stackrel{*}{\leftrightarrow}</math>. El problema de la paraula per a un sistema abstracte de reescriptura és, en general, [[Indecidibilitat|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 <math>x \stackrel{*}{\rightarrow} z \stackrel{*}{\leftarrow} y</math>. A partir d'aquesta definició, sembla natural definir la relació d'unibilitat com <math>\stackrel{*}{\rightarrow} \circ \stackrel{*}{\leftarrow}</math>, on <math>\circ</math> és la [[Composició de funcions|composició]] de relacions. La unibilitat es denota habitualment, d'una forma una mica confusa, amb el símbol <math>\downarrow</math>, però en aquesta notació la fletxa cap avall és un operador binari, és a dir, hom escriu <math>x\mathbin\downarrow y</math> 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]] <math>x \stackrel{*}{\leftrightarrow} y</math> implica que <math>x\mathbin\downarrow y</math> 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;<ref>Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans.
AMS, 39:472-482, 1936</ref> d'aquí el nom de la propietat.{{sfn|Baader|Nipkow|1998|p=9}} (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 [[Reducció beta|reduccions beta]] (''λx''.''xx'')(''λx''.''xx'') → (''λx''.''xx'')(''λx''.''xx'') → ...<ref>{{ref-llibre|cognom=Cooper|nom=S. Barry|títol=Computability theory|pàgina=184|data=17 novembre 2003|isbn=978-1584882374|editorial=Chapman and Hall/CRC}}</ref>

== 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 <math>(A,\rightarrow)</math> és:
* '''confluent''' si i només si per a qualssevol ''w'', ''x'' i ''y'' d{{'}}''A'', <math>x \stackrel{*}{\leftarrow} w \stackrel{*}{\rightarrow} y</math> implica <math>x\mathbin\downarrow y</math>. 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'', <math>x \leftarrow w \stackrel{*}{\rightarrow} y</math> implica <math>x\mathbin\downarrow y</math>. 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'', <math>x \leftarrow w \rightarrow y</math> implica <math>x\mathbin\downarrow y</math>. 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:
<ol style="list-style-type:lower-roman">
 <li>té la propietat de Church-Rosser</li>
 <li>és confluent</li>
 <li>és semi-confluent.{{sfn|Baader|Nipkow|1998|p=11}}</li>
</ol>

'''Corol·lari:'''{{sfn|Baader|Nipkow|1998|p=12}} En un sistema abstracte de reescriptura confluent, si <math>x \stackrel{*}{\leftrightarrow} y</math> llavors
* Si ''x'' i ''y'' són formes normals, llavors ''x'' = ''y''.
* Si ''y'' és una forma normal, llavors <math>x \stackrel{*}{\rightarrow} y</math>

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.{{sfn|Bezem|Klop|de Vrijer|2003|p=11|ref=Terese}} Arran del corol·lari anterior, hom pot definir una forma normal ''y'' d{{'}}''x'' com un ''y'' irreductible tal que <math>x \stackrel{*}{\leftrightarrow} y</math>. Aquesta definició, que es pot trobar a {{harvnb|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 <math>\{a\rightarrow b, b\rightarrow a, a\rightarrow x, b\rightarrow y\}</math>, 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 <math>x_0 \rightarrow x_1 \rightarrow x_2 \rightarrow \cdots</math> (això és equivalent a dir que la relació de reescriptura és una [[Ordre ben fonamentat|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|exemple]] anterior, existeix una cadena infinita (<math>a \rightarrow b \rightarrow a \rightarrow b \rightarrow \cdots</math>), encara que el sistema és normalitzant. Si un sistema abstracte de reescriptura és confluent i noetherià, hom diu que el sistema és '''canònic'''<ref>{{ref-llibre| cognom=Duffy|nom=David A.| títol=Principles of Automated Theorem Proving| any=1991| editorial=Wiley|capítol=secció 7.2.1|pàgina=153}}</ref> 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|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 <math>\rightarrow</math> és terminant, hom pot aplicar [[Ordre ben fonamentat#Inducció i recursió|inducció ben fonamentada]].<ref>{{ref-llibre|cognom=Harrison|nom=John|títol=Handbook of Practical Logic and Automated Reasoning|editorial=[[Cambridge University Press]]|any=2009|isbn=978-0-521-89957-4|capítol=chapter 4 "Equality"|pàgina=260}}</ref>

== Referències ==
{{Referències}}

== Bibliografia ==
* {{ref-llibre|nom=Franz|cognom=Baader|nom2=Tobias|cognom2=Nipkow|títol=Term Rewriting and All That|any=1998|editorial=Cambridge University Press}}
* [[Nachum Dershowitz]] and [[Jean-Pierre Jouannaud]] [http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.3114 ''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.
* {{ref-llibre|cognom=Book|nom=Ronald V.|cognom2=Otto|nom2=Friedrich|títol=String-rewriting Systems|editorial=Springer|any=1993|capítol=Chapter 1, "Abstract reduction systems"}}
* {{ref-llibre|cognom=Bezem|nom=Marc|cognom2=Klop|nom2=Jan Willem|cognom3=de Vrijer|nom3=Roel|títol=Term rewriting systems ("Terese")|editorial=[[Cambridge University Press]]|any=2003|isbn=0-521-39115-6|capítol=Chapter 1|ref=Terese}}
* [[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.; [http://downloads.hindawi.com/journals/ijmms/2010/458563.pdf "The 3x+1 Problem as a String Rewriting System"], ''International Journal of Mathematics and Mathematical Sciences'', Volume 2010 (2010), Article ID 458563, 6 pages.

[[Categoria:Llenguatges formals]]
[[Categoria:Lògica matemàtica]]
[[Categoria:Informàtica teòrica]]