Automatically proving termination and innermost normalisation of term rewriting systems
Thomas Arts · Utrecht University Repository (Utrecht University) · 2001
De Nederlandse samenvatting van een proefschrift is bij uitstek het onderdeel van het proefschrift dat door familie en vrienden wordt gelezen. Voor hen wil ik deze samenvatting dan ook schrijven als een informele inleiding. De samenvatting moet echter ook, zoals het woord al zegt, een korte omschrijving bevatten van de resultaten in dit proefschrift, zodanig dat vakgenoten snel een indruk van deze resultaten kunnen krijgen. Ik heb er voor gekozen het een te doen en het ander niet te laten. Eerst geef ik een informele inleiding die mijn onderzoek in een context plaatst. Daarna volgt een korte beschrijving van de behaalde resultaten. Informele inleiding De vraag die ten grondslag ligt aan de theorie in dit proefschrift is: `Hoe kan een algemene uitspraak over het gedrag van een computerprogramma worden bewezen?'. Als een computerprogramma wordt geschreven moet het aan bepaalde voorwaarden voldoen. Deze voorwaarden liggen vast in de taakomschrijving van het programma. Zo moet een programma dat salarissen berekent voor twee identieke situaties twee identieke salarissen berekenen en zeker niet met twee verschillende uitkomsten komen aanzetten. Een programma dat een vliegtuig bestuurt moet telkens alle vluchtgege- vens beschouwen en mag dus niet enkele minuten bezig blijven met het bepalen van de hoogte en alle andere handelingen opschorten. Een algemene eigenschap waaraan een programma moet voldoen kan doorgaans niet worden bewezen door het programma uitvoerig te testen. Door te testen kunnen ongewenste eigenschappen, fouten, worden opgemerkt. Als het testen echter geen fouten oplevert is daarmee nog niet bewezen dat er geen fouten in het programma aanwezig zijn, alleen dat er geen gevonden zijn. Het probleem bij testen is dat het in het algemeen ondoenlijk is om alle mogelijke invoer en alle randcondities in testen te verwerken. Om zekerheid te krijgen over het gedrag van een programma moet het programma geanalyseerd worden. Dit kan bijvoorbeeld door een model van het programma te ma- ken en de gewenste eigenschap in termen van dit model te vertalen. In dat geval kan een eigenschap van het programma bewezen worden door te bewijzen dat de verta- 169?Samenvatting ling van die eigenschap binnen het model geldt. In het bijzonder bij het wiskundig modelleren van een programma kan een eigenschap met wiskundige zekerheid worden bewezen. Deze aanpak is heel goed vergelijkbaar met de aanpak in andere disciplines. Wanneer een architekt wil bewijzen dat een brug sterk genoeg is, zal een wiskundig model van die brug worden opgesteld. Binnen dat model is het mogelijk de sterkte te berekenen. Een astronoom die wil bewijzen dat de zwaartekracht op Jupiter groter is dan op aarde, zal dat aantonen met behulp van een wiskundig model. Termherschrijfsystemen (in het Engels `term rewriting systems') zijn zeer geschikt voor het modelleren van computerprogramma's. Eigenschappen van een computer- programma kunnen bewezen worden door eigenschappen van het modellerend term- herschrijfsysteem te bewijzen. In dit proefschrift staan twee eigenschappen van term- herschrijfsystemen centraal: terminatie en innermost normalisatie (een variant van terminatie). Door het bewijzen van terminatie van een termherschrijfsysteem kan be- wezen worden dat een programma gegarandeerd stopt na enige tijd. Daarmee wordt de zekerheid verkregen dat dit programma niet `hangt' (een term voor een computer- programma dat vast zit en ogenschijnlijk niets meer doet). Ook andere eigenschappen van een programma kunnen worden bewezen door te bewijzen dat een bepaald term- herschrijfsysteem termineert. Zo is het mogelijk een bewijs dat een termherschrijf- systeem termineert te gebruiken om te bewijzen dat de uitkomst van een door het gemodelleerde programma uitgevoerde berekening uniek is. Met het kunnen bewijzen van terminatie van een termherschrijfsysteem kan dus iets geconcludeerd worden over het gedrag van een programma. Op de vraag hoe de terminatie van een termherschrijfsysteem bewezen kan worden, geeft dit proefschrift een antwoord. Aan de hand van een voorbeeld zal ik duidelijk maken hoe een programma gemo- delleerd kan worden door een termherschrijfsysteem en hoe een bewijs van terminatie van dat systeem iets kan vertellen over het gedrag van het programma. Ik merk daar- bij op dat het hier slechts om een voorbeeld gaat en dat de theorie en technieken in dit proefschrift veel meer omvatten dan alleen een oplossing voor het probleem geschetst in dit voorbeeld. Voor het voorbeeld beschouwen we het programma waarmee dit proefschrift is gezet, namelijk T E X. Het programma T E X maakt van een ingetypte tekst een op- gemaakte pagina, klaar voor de pers. Het programma is ontworpen als een `open' programma. Dat wil zeggen dat iedereen er in principe iets aan toe mag voegen. Het Arabisch of Chinees schrift zijn typisch dingen om aanT E X toe te voegen. Het toevoegen van een schrift omvat meer dan alleen het toevoegen van de afzonderlijke letters of symbolen van dat schrift. Het is bijvoorbeeld ook nodig om informatie van elkaar opvolgende symbolen aan T E X kenbaar te maken. Zo is T E X voorzien van de informatie dat in het schrift waarin dit proefschrift gedrukt is de `f' aan de `l' vast geschreven wordt. Dit is goed te zien in een woord als ` orijn', dat zonder deze extra informatie zou worden geschreven als `florijn'. Op een zelfde manier worden twee opeenvolgende letters `f' aan elkaar vast geschreven en het puntje van een `i' die op 170?Samenvatting orijn florijn Figuur 10.1: De ligatuur ` ' in het woord ` orijn' een `f ' volgt wordt door de `f' overdekt. Deze ligaturen zijn goed zichtbaar in het woord ache in plaats van affiche: De informatie bij de denitie van het schrift vertelt T E X omtwee opeenvolgende letters `f ' door de ligatuur `' te vervangen. In de wat oudere versies van het programma T E X waren de ligatuur mogelijkheden vrij beperkt, maar in elk geval kon de ontwikkelaar van een nieuw schrift aangeven welke symbolen door welke ligatuur moesten worden vervangen. Deze informatie kan bijvoorbeeld worden beschreven als f f ! f l ! : Het algemene schema van de ligatuur informatie kan worden beschreven als ! waar , en symbolen zijn (waarbij typisch een ligatuur is, maar en mogen ook ligaturen zijn). Dit schema wordt een termherschrijfsysteem door voor de 's 's en 's daadwerkelijke symbolen in te vullen, zoals in het geval van de `' en ` '. Een termherschrijfsysteem bestaat uit een aantal regels die aangeven wat waardoor vervangen moet worden. Een termherschrijfsysteem dat bestaat uit instantiaties van de regel in het bo- venstaande schema beschrijft op deze manier welke symbolen door welke ligatuur moeten worden vervangen om de juiste typograe te bereiken. Door de regels van het herschrijf systeem f i ! f f ! i ! ? e ! ?e herhaaldelijk toe te passen op het woord `effici?ent' wordt dit herschreven tot `eci?ent' effici?ent ! eici?ent ! eci?ent ! eci?ent: Merk op dat het vervangen van opeenvolgende symbolen niet noodzakelijkerwijs een uniek proces is. In het bovenstaande voorbeeld worden eerst twee opeenvolgende `f'-en door de ligatuur `' vervangen. De combinatie `fi' had echter ook eerst door 171?Samenvatting de ligatuur `' kunnen worden vervangen. In dat laatste geval had `f' gevolgd door de ligatuur `' niet vervangen kunnen worden door de ligatuur `', omdat daar geen regel voor bestaat in dit gegeven termherschrijfsysteem. Samengevat kan de ligatuur informatie beschreven worden door een termherschrijf- systeem. Zo'n termherschrijfsysteem is niet alleen een model voor die informatie, het kan zelfs gebruikt worden om alle ligaturen in een woord te berekenen door middel van `herschrijvingen'. Voor het zetten van teksten in het Arabisch of het Chinees is meer geavanceerde ligatuur informatie nodig dan met het bovengenoemde schema voor ligatuur infor- matie uitgedrukt kan worden. Daarom is er aan nieuwere versies van T E X een ander ligatuur mechanisme toegevoegd. Behalve het vervangen van twee symbolen door een ligatuur kan nu ookeen enkel symbool door een ligatuur worden vervangen of kan er tussen twee symbolen een ligatuur worden geplaatst. Deze informele beschrijving van de ligatuur informatie kan weer formeel worden uitgedrukt in een schema ! ! ! ! : Door , en te vervangen door geschikte symbolen zijn uit dit schema weer ver- schillende termherschrijfsystemen te vormen. Merk op dat niet voor alle 's, 's en 's dezelfde symbolen hoeven worden ingevuld. Net als in het vorige voorbeeld kan zo'n termherschrijfsysteem bijvoorbeeld gevormd worden door alleen de eerste regel te gebruiken en voor de 's, 's en 's telkens iets ander in te vullen. Het verschil is nu dat er ook regels mogen worden toegevoegd die een invulling zijn van een van de andere drie regels in het schema. In deze uitbreiding van het ligatuur mechanisme schuilt een gevaar. Een zorgeloze ontwerper van een nieuw schrift kan dat schrift ligatuur informatie meegeven die het programma dat de ligatuur moet berekenen in een oneindige lus brengt. Het programma blijft in zo'n geval rekenen zonder een juiste ligatuur te vinden. Stel maar dat een schrift drie symbolen bevat `a', `b' en `c' die de volgende ligatuur informatie meekrijgen: a b ! a c a c ! a bc dan kan het woord `ab' oneindig vaak herschreven worden a b! a c! a bc! a cc! a b c c! a ccc! : : : In termen van het programma betekent dit dat T E X door deze ligatuur informatie bij het zetten van het woord `ab' in een oneindige lus raakt en het programma daardoor hangt. De reden om dit gevaar te accepteren en het nieuwe ligatuur meganisme te gebruiken in plaats van het oude, is dat door de verkregen vrijheid bepaalde ligaturen 172?Samenvatting in het Arabisch en Chinees hierdoor te beschrijven zijn. Voor deze vergroting van de uitdrukkingskracht wordt de prijs betaald dat er ook dingen beschreven kunnen worden die niet voor mogen komen. Het formaliseren van de ligatuur informatie maakt het mogelijk om het gedrag te beschri