Herschrijven (theoretische informatica)

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

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:

$(42+3)/(7-2)=45/(7-2)=45/5=9$

Sommige rekenkundige bewerkingen staan twee verschillende stappen toe. Uit $(42+3)/(7-2)$ kunnen we met een enkele stap niet alleen $45/(7-2)$ afleiden, maar ook $(42+3)/5$. Sommige rekenkundige uitdrukkingen kunnen helemaal niet verder vereenvoudigd worden, bijvoorbeeld $9$. Zo'n uitdrukking wordt normaalvorm genoemd en representeert als het ware de uitkomst van een berekening.

Vormen van herschrijven

Herschrijven in het algemeen

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 $A$ (de verzameling van objecten die herschreven kunnen worden) en een tweeplaatsige relatie op $A$ (de herschrijfrelatie), die meestal als $\rightarrow$ wordt geschreven. We schrijven dus $a\rightarrow b$ als het object $a$ in één stap naar het object $b$ 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:

• $\leftarrow$ is de inverse van $\rightarrow$, dat wil zeggen, $a\leftarrow b$ geldt precies dan als $b\rightarrow a$;
• ${\leftrightarrow }={\rightarrow }\cup {\rightarrow }$, dat wil zeggen dat $a\leftrightarrow b$ geldt als $a\rightarrow b$ of $a\leftarrow b$
• $\rightarrow ^{*}$, $\leftarrow ^{*}$ en $\leftrightarrow ^{*}$ zijn de reflexief-transitieve afsluitingen van respectievelijk $\rightarrow$, $\leftarrow$ en $\leftrightarrow$. Dat betekent bijvoorbeeld dat $a\rightarrow ^{*}b$ als $b$ in nul of meer stappen uit $a$ bereikt kan worden.

Termherschrijven

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

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

• Een variabele $x\in X$ is een term.
• Als $f\in \Sigma$ een $n$-plaatsig functiesymbool is, en $t_{1},\ldots ,t_{n}$ termen, dan is $f(t_{1},\ldots ,t_{n})$ een term. Tweeplaatsige functiesymbolen worden ook vaak tussen hun argumenten genoteerd, bijvoorbeeld $(t_{1}+t_{2})$ in plaats van $+(t_{1},t_{2})$.

Voorbeelden van termen zijn logische formules ($\Sigma =\{{\land },{\lor },{\rightarrow },{\leftrightarrow },{\neg }\}$) en rekenkundige expressies ($\Sigma =\{{+},{-},{\times },{/},\ldots \}$).

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

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

Voorbeeld: Optellen

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

Optellen kan nu worden gedefinieerd met het volgende termherschrijfsysteem:

${\begin{array}{rcl}{\mathsf {plus}}(x,{\mathsf {0}})&\rightarrow &x\\{\mathsf {plus}}(x,{\mathsf {s}}(y))&\rightarrow &{\mathsf {s}}({\mathsf {plus}}(x,y))\end{array}}$

Met dit herschrijfsysteem kunnen we bijvoorbeeld $1+2$ berekenen:

${\mathsf {plus}}({\mathsf {s}}({\mathsf {0}}),{\mathsf {s}}({\mathsf {s}}({\mathsf {0}})))\rightarrow {\mathsf {s}}({\mathsf {plus}}({\mathsf {s}}({\mathsf {0}}),{\mathsf {s}}({\mathsf {0}})))\rightarrow {\mathsf {s}}({\mathsf {s}}({\mathsf {plus}}({\mathsf {s}}({\mathsf {0}}),{\mathsf {0}})))\rightarrow {\mathsf {s}}({\mathsf {s}}({\mathsf {s}}({\mathsf {0}})))$

Hogere-orde-termherschrijven

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

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

Terminatie en normalisatie

Een normaalvorm van een object $a$ is een object $b$ dat zelf niet herschreven kan worden en waarvoor geldt dat $a\rightarrow ^{*}b$. Een (abstract) herschrijfsysteem heet normaliserend wanneer elk object een normaalvorm heeft. In het geval dat een object $a$ precies één normaalvorm heeft spreken we ook wel over de normaalvorm van $a$, geschreven $a{\downarrow }$.

Een herschrijfsysteem is terminerend wanneer het geen oneindige herschrijfrijtjes toelaat, dat wil zeggen dat er geen oneindige rijtjes $a_{1},a_{2},\ldots$ bestaan zodat $a_{i}\rightarrow a_{i+1}$ voor alle $i\geq 0$.

Een terminerend herschrijfsysteem is noodzakelijkerwijs ook normaliserend. Om voor een willekeurig object $a$ 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 $a$. 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 $0\rightarrow 0,0\rightarrow 1$. Dit systeem is normaliserend, omdat de normaalvorm 1 vanaf beide objecten bereikt kan worden. Het is echter niet terminerend vanwege de oneindige herschrijfrij $0\rightarrow 0\rightarrow \cdots$.

Confluentie en de stelling van Church-Rosser

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

• Confluentie. Een herschrijfsysteem is confluent wanneer geldt dat als $a\rightarrow ^{*}b$ en $a\rightarrow ^{*}c$, er dan een $d$ moet bestaan zodat $b\rightarrow ^{*}d$ en $c\rightarrow ^{*}d$.
• Lokale confluentie. Een herschrijfsysteem is lokaal confluent wanneer geldt dat als $a\rightarrow b$ en $a\rightarrow c$, er dan een $d$ moet bestaan zodat $b\rightarrow ^{*}d$ en $c\rightarrow ^{*}d$.
• Church-Rosser-eigenschap. Een herschrijfsysteem heeft de Church-Rosser-eigenschap, als geldt dat $a\leftrightarrow ^{*}b$ impliceert dat er een $c$ bestaat zodat $a\rightarrow ^{*}c$ en $b\rightarrow ^{*}c$.

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

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

Literatuur

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