Herschrijven (theoretische informatica)

Uit Wikipedia, de vrije encyclopedie
Naar navigatie springen Naar zoeken springen

In de theoretische informatica is herschrijven (Engels: rewriting) een onderzoeksgebied dat zich bezighoudt met stapsgewijze, discrete transformaties van objecten, vaak met het doel een bepaald eindresultaat (bijvoorbeeld de uitkomst van een berekening) te bereiken. De mogelijke stappen die genomen kunnen worden, worden gespecificeerd in een herschrijfsysteem. Herschrijfsystemen zijn vaak niet-deterministisch: het wordt niet voorgeschreven welke van de mogelijke stappen de volgende stap is.

Er bestaan verschillende vormen van herschrijven, bijvoorbeeld termherschrijven, graafherschrijven en stringherschrijven.

Informeel voorbeeld[bewerken | brontekst bewerken]

Rekenen met optellen, aftrekken, vermenigvuldigen en delen kan als herschrijfsysteem worden gemodelleerd. De objecten die herschreven worden zijn rekenkundige uitdrukkingen, terwijl in een herschrijfstap één rekenkundige bewerking kan worden uitgevoerd. Zo bestaat bijvoorbeeld de volgende herschrijfrij:

Sommige rekenkundige bewerkingen staan twee verschillende stappen toe. Uit kunnen we met een enkele stap niet alleen afleiden, maar ook . Sommige rekenkundige uitdrukkingen kunnen helemaal niet verder vereenvoudigd worden, bijvoorbeeld . Zo'n uitdrukking wordt normaalvorm genoemd en representeert als het ware de uitkomst van een berekening.

Vormen van herschrijven[bewerken | brontekst bewerken]

Herschrijven in het algemeen[bewerken | brontekst bewerken]

Er bestaan herschrijfsystemen die met verschillende soorten objecten werken, zoals termen, strings of grafen. Herschrijfsystemen hebben echter een aantal eigenschappen met elkaar gemeen. Om deze algemene eigenschappen te definiëren en te onderzoeken worden abstracte herschrijfsystemen gebruikt. In een abstract herschrijfsysteem wordt geabstraheerd van het specifieke object waarmee het systeem werkt. Een abstract herschrijfsysteem bestaat uit een verzameling (de verzameling van objecten die herschreven kunnen worden) en een tweeplaatsige relatie op (de herschrijfrelatie), die meestal als wordt geschreven. We schrijven dus als het object in één stap naar het object herschreven kan worden.

De herschrijfrelatie bevat de mogelijke atomaire stappen die genomen kunnen worden. Op basis van de herschrijfrelatie kunnen we afgeleide relaties definiëren:

  • is de inverse van , dat wil zeggen, geldt precies dan als ;
  • , dat wil zeggen dat geldt als of
  • , en zijn de reflexief-transitieve afsluitingen van respectievelijk , en . Dat betekent bijvoorbeeld dat als in nul of meer stappen uit bereikt kan worden.

Termherschrijven[bewerken | brontekst bewerken]

Bij termherschrijven zijn de objecten die herschreven worden termen. Termen bestaan uit functiesymbolen en operatoren, constanten en variabelen, zoals bijvoorbeeld rekenkundige uitdrukkingen en logische formules.

Definitie[bewerken | brontekst bewerken]

De taal van een term wordt gegeven door een zogenaamde signatuur. Een signatuur is een eindige verzameling van functiesymbolen, waarbij aan elk functiesymbool een plaatsigheid toegekend is. Gegeven een signatuur en een oneindige verzameling van variabelen, wordt een (eerste-orde) term inductief gedefinieerd door:

  • Een variabele is een term.
  • Als een -plaatsig functiesymbool is, en termen, dan is een term. Tweeplaatsige functiesymbolen worden ook vaak tussen hun argumenten genoteerd, bijvoorbeeld in plaats van .

Voorbeelden van termen zijn logische formules () en rekenkundige expressies ().

Een termherschrijfsysteem bestaat uit een eindig aantal termherschrijfregels. Elke herschrijfregel is van de vorm , waarbij en termen zijn en alle variabelen die in voorkomen óók in voorkomen. In een regel wordt de linkerkant en de rechterkant genoemd. We kunnen een herschrijfregel op een term toepassen door:

  • eerst de variabelen in en door willekeurige termen te vervangen, waarbij dezelfde variabele wel altijd door dezelfde term moet worden vervangen;
  • een voorkomen van de linkerkant in te zoeken;
  • en ten slotte dit voorkomen door de rechterkant te vervangen.

Voorbeeld: Optellen[bewerken | brontekst bewerken]

We beschouwen de signatuur , waarbij 0-plaatsig is (dat wil zeggen: het is een constante), 1-plaatsig en 2-plaatsig. Hoewel termherschrijven een zuiver syntactische bezigheid is, kunnen we, om het voorbeeld beter te begrijpen, de termen als volgt interpreteren: is het getal 0, is de opvolgerfunctie (dus betekent 1, en betekent 2) en is de optelfunctie.

Optellen kan nu worden gedefinieerd met het volgende termherschrijfsysteem:

Met dit herschrijfsysteem kunnen we bijvoorbeeld berekenen:

Hogere-orde-termherschrijven[bewerken | brontekst bewerken]

Er bestaan ook varianten van termherschrijven waarbij gebonden variabelen kunnen voorkomen. Dit maakt het mogelijk ook hogere-orde-bewerkingen te modelleren, bijvoorbeeld de map-operatie die een functie op alle elementen van een lijst toepast. Om deze reden worden zulkte termherschrijfsystemen hogere-orde-termherschrijfsystemen genoemd. Een bekend voorbeeld van een hogere-orde-termherschrijfsysteem is de lambdacalculus.

Graafherschrijven[bewerken | brontekst bewerken]

Bij graafherschrijven zijn de objecten die herschreven worden grafen. Bij graafherschrijven zoeken we de linkerkant van een graafherschrijfregel als ondergraaf in de te herschrijven graaf en vervangen deze door de rechterkant van de regel.

Eigenschappen van herschijfsystemen[bewerken | brontekst bewerken]

Terminatie en normalisatie[bewerken | brontekst bewerken]

Een normaalvorm van een object is een object dat zelf niet herschreven kan worden en waarvoor geldt dat . Een (abstract) herschrijfsysteem heet normaliserend wanneer elk object een normaalvorm heeft. In het geval dat een object precies één normaalvorm heeft spreken we ook wel over de normaalvorm van , geschreven .

Een herschrijfsysteem is terminerend wanneer het geen oneindige herschrijfrijtjes toelaat, dat wil zeggen dat er geen oneindige rijtjes bestaan zodat voor alle .

Een terminerend herschrijfsysteem is noodzakelijkerwijs ook normaliserend. Om voor een willekeurig object een normaalvorm te vinden, kunnen we herschrijfstappen uitvoeren totdat we een object bereikt hebben dat niet verder te herschrijven is. Dat is dan een normaalvorm van . Omdat het herschrijfsysteem termineert bereiken we ook altijd een normaalvorm. Andersom is echter niet het geval: er bestaan herschrijfsystemen die weliswaar normaliserend zijn, maar niet termineren. Neem bijvoorbeeld het abstract herschrijfsysteem dat uit de objecten 0 en 1 en de herschrijfrelatie . Dit systeem is normaliserend, omdat de normaalvorm 1 vanaf beide objecten bereikt kan worden. Het is echter niet terminerend vanwege de oneindige herschrijfrij .

Confluentie en de stelling van Church-Rosser[bewerken | brontekst bewerken]

We beschouwen de volgende mogelijke eigenschappen van (abstracte) herschrijfsystemen:

  • Confluentie. Een herschrijfsysteem is confluent wanneer geldt dat als en , er dan een moet bestaan zodat en .
  • Lokale confluentie. Een herschrijfsysteem is lokaal confluent wanneer geldt dat als en , er dan een moet bestaan zodat en .
  • Church-Rosser-eigenschap. Een herschrijfsysteem heeft de Church-Rosser-eigenschap, als geldt dat impliceert dat er een bestaat zodat en .

Het is triviaal het geval dat een confluent herschrijfsysteem ook lokaal confluent is. Andersom is dit echter niet het geval: er bestaan lokaal confluente herschrijfsystemen die niet confluent zijn. Max Newman bewees in 1942 echter wel Newmans lemma: voor een terminerend herschrijfsysteem geldt wél dat als het systeem lokaal confluent is, het ook confluent is.

Confluentie en de Church-Rosser-eigenschap zijn op het eerste gezicht verschillende eigenschappen. In 1936 bewees Alonzo Church samen met zijn student John Barkley Rosser echter dat de twee eigenschappen samenvallen. Deze stelling wordt de Stelling van Church-Rosser genoemd.

Het woordprobleem[bewerken | brontekst bewerken]

Het woordprobleem voor een herschrijfsysteem is het beslissingsprobleem dat, gegeven twee objecten en van dat herschrijfsysteem, de vraag stelt of . In het algemeen is het woordprobleem op herschrijfsystemen onbeslisbaar. Als echter terminerend en confluent is, is het woordprobleem voor beslisbaar: we kunnen beide objecten tot hun normaalvorm reduceren. Er geldt dan en slechts dan als beide objecten dezelfde normaalvorm hebben.

Literatuur[bewerken | brontekst bewerken]

  • Terese. Term Rewriting Systems. Cambridge University Press, 2003
  • Franz Baader en Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998