Automatically proving termination and innermost normalisation of term rewriting systems

Abstract

De Nederlandse samenvatting van een proefschrift is bij uitstek het onderdeel van
\nhet proefschrift dat door familie en vrienden wordt gelezen. Voor hen wil ik deze
\nsamenvatting dan ook schrijven als een informele inleiding. De samenvatting moet
\nechter ook, zoals het woord al zegt, een korte omschrijving bevatten van de resultaten
\nin dit proefschrift, zodanig dat vakgenoten snel een indruk van deze resultaten kunnen
\nkrijgen. Ik heb er voor gekozen het een te doen en het ander niet te laten. Eerst geef
\nik een informele inleiding die mijn onderzoek in een context plaatst. Daarna volgt
\neen korte beschrijving van de behaalde resultaten.
\nInformele inleiding
\nDe vraag die ten grondslag ligt aan de theorie in dit proefschrift is: `Hoe kan een
\nalgemene uitspraak over het gedrag van een computerprogramma worden bewezen?'.
\nAls een computerprogramma wordt geschreven moet het aan bepaalde voorwaarden
\nvoldoen. Deze voorwaarden liggen vast in de taakomschrijving van het programma.
\nZo moet een programma dat salarissen berekent voor twee identieke situaties twee
\nidentieke salarissen berekenen en zeker niet met twee verschillende uitkomsten komen
\naanzetten. Een programma dat een vliegtuig bestuurt moet telkens alle vluchtgege-
\nvens beschouwen en mag dus niet enkele minuten bezig blijven met het bepalen van de
\nhoogte en alle andere handelingen opschorten. Een algemene eigenschap waaraan een
\nprogramma moet voldoen kan doorgaans niet worden bewezen door het programma
\nuitvoerig te testen. Door te testen kunnen ongewenste eigenschappen, fouten, worden
\nopgemerkt. Als het testen echter geen fouten oplevert is daarmee nog niet bewezen
\ndat er geen fouten in het programma aanwezig zijn, alleen dat er geen gevonden zijn.
\nHet probleem bij testen is dat het in het algemeen ondoenlijk is om alle mogelijke
\ninvoer en alle randcondities in testen te verwerken.
\nOm zekerheid te krijgen over het gedrag van een programma moet het programma
\ngeanalyseerd worden. Dit kan bijvoorbeeld door een model van het programma te ma-
\nken en de gewenste eigenschap in termen van dit model te vertalen. In dat geval kan
\neen eigenschap van het programma bewezen worden door te bewijzen dat de verta-
\n169?Samenvatting
\nling van die eigenschap binnen het model geldt. In het bijzonder bij het wiskundig
\nmodelleren van een programma kan een eigenschap met wiskundige zekerheid worden
\nbewezen. Deze aanpak is heel goed vergelijkbaar met de aanpak in andere disciplines.
\nWanneer een architekt wil bewijzen dat een brug sterk genoeg is, zal een wiskundig
\nmodel van die brug worden opgesteld. Binnen dat model is het mogelijk de sterkte te
\nberekenen. Een astronoom die wil bewijzen dat de zwaartekracht op Jupiter groter
\nis dan op aarde, zal dat aantonen met behulp van een wiskundig model.
\nTermherschrijfsystemen (in het Engels `term rewriting systems') zijn zeer geschikt
\nvoor het modelleren van computerprogramma's. Eigenschappen van een computer-
\nprogramma kunnen bewezen worden door eigenschappen van het modellerend term-
\nherschrijfsysteem te bewijzen. In dit proefschrift staan twee eigenschappen van term-
\nherschrijfsystemen centraal: terminatie en innermost normalisatie (een variant van
\nterminatie). Door het bewijzen van terminatie van een termherschrijfsysteem kan be-
\nwezen worden dat een programma gegarandeerd stopt na enige tijd. Daarmee wordt
\nde zekerheid verkregen dat dit programma niet `hangt' (een term voor een computer-
\nprogramma dat vast zit en ogenschijnlijk niets meer doet). Ook andere eigenschappen
\nvan een programma kunnen worden bewezen door te bewijzen dat een bepaald term-
\nherschrijfsysteem termineert. Zo is het mogelijk een bewijs dat een termherschrijf-
\nsysteem termineert te gebruiken om te bewijzen dat de uitkomst van een door het
\ngemodelleerde programma uitgevoerde berekening uniek is.
\nMet het kunnen bewijzen van terminatie van een termherschrijfsysteem kan dus
\niets geconcludeerd worden over het gedrag van een programma. Op de vraag hoe de
\nterminatie van een termherschrijfsysteem bewezen kan worden, geeft dit proefschrift
\neen antwoord.
\nAan de hand van een voorbeeld zal ik duidelijk maken hoe een programma gemo-
\ndelleerd kan worden door een termherschrijfsysteem en hoe een bewijs van terminatie
\nvan dat systeem iets kan vertellen over het gedrag van het programma. Ik merk daar-
\nbij op dat het hier slechts om een voorbeeld gaat en dat de theorie en technieken in dit
\nproefschrift veel meer omvatten dan alleen een oplossing voor het probleem geschetst
\nin dit voorbeeld.
\nVoor het voorbeeld beschouwen we het programma waarmee dit proefschrift is
\ngezet, namelijk T E X. Het programma T E X maakt van een ingetypte tekst een op-
\ngemaakte pagina, klaar voor de pers. Het programma is ontworpen als een `open'
\nprogramma. Dat wil zeggen dat iedereen er in principe iets aan toe mag voegen.
\nHet Arabisch of Chinees schrift zijn typisch dingen om aanT E X toe te voegen. Het
\ntoevoegen van een schrift omvat meer dan alleen het toevoegen van de afzonderlijke
\nletters of symbolen van dat schrift. Het is bijvoorbeeld ook nodig om informatie van
\nelkaar opvolgende symbolen aan T E X kenbaar te maken. Zo is T E X voorzien van de
\ninformatie dat in het schrift waarin dit proefschrift gedrukt is de `f' aan de `l' vast
\ngeschreven wordt. Dit is goed te zien in een woord als ` orijn', dat zonder deze extra
\ninformatie zou worden geschreven als `florijn'. Op een zelfde manier worden twee
\nopeenvolgende letters `f' aan elkaar vast geschreven en het puntje van een `i' die op
\n170?Samenvatting
\norijn florijn
\nFiguur 10.1: De ligatuur ` ' in het woord ` orijn'
\neen `f ' volgt wordt door de `f' overdekt. Deze ligaturen zijn goed zichtbaar in het
\nwoord
\nache in plaats van affiche:
\nDe informatie bij de denitie van het schrift vertelt T E X omtwee opeenvolgende letters
\n`f ' door de ligatuur `' te vervangen. In de wat oudere versies van het programma T E X
\nwaren de ligatuur mogelijkheden vrij beperkt, maar in elk geval kon de ontwikkelaar
\nvan een nieuw schrift aangeven welke symbolen door welke ligatuur moesten worden
\nvervangen. Deze informatie kan bijvoorbeeld worden beschreven als
\nf f ! 
\nf l ! :
\nHet algemene schema van de ligatuur informatie kan worden beschreven als
\n ! 
\nwaar , en symbolen zijn (waarbij typisch een ligatuur is, maar en mogen
\nook ligaturen zijn). Dit schema wordt een termherschrijfsysteem door voor de 's
\n's en 's daadwerkelijke symbolen in te vullen, zoals in het geval van de `' en ` '.
\nEen termherschrijfsysteem bestaat uit een aantal regels die aangeven wat waardoor
\nvervangen moet worden.
\nEen termherschrijfsysteem dat bestaat uit instantiaties van de regel in het bo-
\nvenstaande schema beschrijft op deze manier welke symbolen door welke ligatuur
\nmoeten worden vervangen om de juiste typograe te bereiken. Door de regels van het
\nherschrijf systeem
\nf i ! 
\nf f ! 
\n i ! 
\n? e ! ?e
\nherhaaldelijk toe te passen op het woord `effici?ent' wordt dit herschreven tot `eci?ent'
\neffici?ent ! eici?ent ! eci?ent ! eci?ent:
\nMerk op dat het vervangen van opeenvolgende symbolen niet noodzakelijkerwijs
\neen uniek proces is. In het bovenstaande voorbeeld worden eerst twee opeenvolgende
\n`f'-en door de ligatuur `' vervangen. De combinatie `fi' had echter ook eerst door
\n171?Samenvatting
\nde ligatuur `' kunnen worden vervangen. In dat laatste geval had `f' gevolgd door
\nde ligatuur `' niet vervangen kunnen worden door de ligatuur `', omdat daar geen
\nregel voor bestaat in dit gegeven termherschrijfsysteem.
\nSamengevat kan de ligatuur informatie beschreven worden door een termherschrijf-
\nsysteem. Zo'n termherschrijfsysteem is niet alleen een model voor die informatie, het
\nkan zelfs gebruikt worden om alle ligaturen in een woord te berekenen door middel
\nvan `herschrijvingen'.
\nVoor het zetten van teksten in het Arabisch of het Chinees is meer geavanceerde
\nligatuur informatie nodig dan met het bovengenoemde schema voor ligatuur infor-
\nmatie uitgedrukt kan worden. Daarom is er aan nieuwere versies van T E X een ander
\nligatuur mechanisme toegevoegd. Behalve het vervangen van twee symbolen door een
\nligatuur kan nu ookeen enkel symbool door een ligatuur worden vervangen of kan er
\ntussen twee symbolen een ligatuur worden geplaatst. Deze informele beschrijving van
\nde ligatuur informatie kan weer formeel worden uitgedrukt in een schema
\n ! 
\n ! 
\n ! 
\n ! :
\nDoor , en te vervangen door geschikte symbolen zijn uit dit schema weer ver-
\nschillende termherschrijfsystemen te vormen. Merk op dat niet voor alle 's, 's en
\n's dezelfde symbolen hoeven worden ingevuld. Net als in het vorige voorbeeld kan
\nzo'n termherschrijfsysteem bijvoorbeeld gevormd worden door alleen de eerste regel
\nte gebruiken en voor de 's, 's en 's telkens iets ander in te vullen. Het verschil is
\nnu dat er ook regels mogen worden toegevoegd die een invulling zijn van een van de
\nandere drie regels in het schema.
\nIn deze uitbreiding van het ligatuur mechanisme schuilt een gevaar. Een zorgeloze
\nontwerper van een nieuw schrift kan dat schrift ligatuur informatie meegeven die
\nhet programma dat de ligatuur moet berekenen in een oneindige lus brengt. Het
\nprogramma blijft in zo'n geval rekenen zonder een juiste ligatuur te vinden. Stel maar
\ndat een schrift drie symbolen bevat `a', `b' en `c' d