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.

Inhoud

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:

\({\displaystyle (42+3)/(7-2)=45/(7-2)=45/5=9}\)

Sommige rekenkundige bewerkingen staan twee verschillende stappen toe. Uit \({\displaystyle (42+3)/(7-2)}\) kunnen we met een enkele stap niet alleen \({\displaystyle 45/(7-2)}\) afleiden, maar ook \({\displaystyle (42+3)/5}\). Sommige rekenkundige uitdrukkingen kunnen helemaal niet verder vereenvoudigd worden, bijvoorbeeld \({\displaystyle 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 \({\displaystyle A}\) (de verzameling van objecten die herschreven kunnen worden) en een tweeplaatsige relatie op \({\displaystyle A}\) (de herschrijfrelatie), die meestal als \({\displaystyle \rightarrow }\) wordt geschreven. We schrijven dus \({\displaystyle a\rightarrow b}\) als het object \({\displaystyle a}\) in één stap naar het object \({\displaystyle 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:

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 \({\displaystyle \Sigma }\) van functiesymbolen, waarbij aan elk functiesymbool \({\displaystyle f\in \Sigma }\) een plaatsigheid toegekend is. Gegeven een signatuur \({\displaystyle \Sigma }\) en een oneindige verzameling \({\displaystyle X}\) van variabelen, wordt een (eerste-orde) term inductief gedefinieerd door:

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

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

Voorbeeld: Optellen

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

Optellen kan nu worden gedefinieerd met het volgende termherschrijfsysteem:

\({\displaystyle {\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 \({\displaystyle 1+2}\) berekenen:

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

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

Een terminerend herschrijfsysteem is noodzakelijkerwijs ook normaliserend. Om voor een willekeurig object \({\displaystyle 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 \({\displaystyle 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 \({\displaystyle 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 \({\displaystyle 0\rightarrow 0\rightarrow \cdots }\).

Confluentie en de stelling van Church-Rosser

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

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 \({\displaystyle A}\) is het beslissingsprobleem dat, gegeven twee objecten \({\displaystyle a}\) en \({\displaystyle b}\) van dat herschrijfsysteem, de vraag stelt of \({\displaystyle a\leftrightarrow ^{*}b}\). In het algemeen is het woordprobleem op herschrijfsystemen onbeslisbaar. Als \({\displaystyle A}\) echter terminerend en confluent is, is het woordprobleem voor \({\displaystyle A}\) beslisbaar: we kunnen beide objecten tot hun normaalvorm reduceren. Er geldt \({\displaystyle a\leftrightarrow ^{*}b}\) dan en slechts dan als beide objecten dezelfde normaalvorm hebben.

Literatuur











Categorieën: Theoretische informatica




Staat van informatie: 26.09.2021 12:13:43 CEST

oorsprong: Wikipedia (Auteurs [Geschiedenis])    Licentie: CC-BY-SA-3.0

Veranderingen: Alle afbeeldingen en de meeste ontwerpelementen die daarmee verband houden, zijn verwijderd. Sommige pictogrammen werden vervangen door FontAwesome-Icons. Sommige sjablonen zijn verwijderd (zoals 'artikel heeft uitbreiding nodig') of toegewezen (zoals 'hatnotes'). CSS-klassen zijn verwijderd of geharmoniseerd.
Specifieke Wikipedia-links die niet naar een artikel of categorie leiden (zoals 'Redlinks', 'links naar de bewerkpagina', 'links naar portals') zijn verwijderd. Elke externe link heeft een extra FontAwesome-Icon. Naast enkele kleine wijzigingen in het ontwerp, werden mediacontainer, kaarten, navigatiedozen, gesproken versies en Geo-microformats verwijderd.

Belangrijke opmerking Omdat de gegeven inhoud op het gegeven moment automatisch van Wikipedia wordt gehaald, was en is een handmatige verificatie niet mogelijk. Daarom garandeert LinkFang.org niet de juistheid en actualiteit van de verkregen inhoud. Als er informatie is die momenteel verkeerd is of een onjuiste weergave heeft, aarzel dan niet om Neem contact op: E-mail.
Zie ook: Afdruk & Privacy policy.