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:

 

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

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  (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 
 
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  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 
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 

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

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 

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 
 Terese. Term Rewriting Systems. Cambridge University Press, 2003
 Franz Baader en Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998

Theoretische informatica