Voorwoord

Dit boek is voortgekomen uit materiaal dat is gebruikt bij colleges op de beide universiteiten in Amsterdam. Een deel van het materiaal is tevens verschillende malen gebruikt bij de PAO-cursus Moderne Technieken in Software Engineering verzorgd door het Centrum voor Wiskunde en Informatica te Amsterdam.

Het boek bevat een overzicht van de theorie van termherschrijfsystemen. Getracht is om alle centrale thema's betreffende termherschrijving te bespreken. Op meer specialistische zaken zoals herschrijven modulo commutativiteit en associativiteit en de verbanden met logisch programmeren wordt echter niet ingegaan.

Ten opzichte van de bestaande overzichtsliteratuur zijn enkele vernieuwingen aangebracht met name betreffende de presentatie van recursive pad ordeningen en correctheidsbewijzen van completerings-algoritmen.

Termherschrijfsystemen krijgen in toenamende mate een centrale plaats binnen de theoretische informatica. Wij behandelen de theorie abstract, dat wil zeggen zonder nadruk op speciale toepassingen.

Termherschrijving wordt inmiddels op allerlei gebieden toegepast. Te vermelden valt: implementatie van abstracte datatypen, automatisch bewijzen van stellingen in wiskundige structuren, automatische verificatie van formele bewijzen, grondslagen van het functioneel programmeren, architecturen van reductiemachines, en uitbreidingen van logisch programmeren.

Internationaal zijn tientallen onderzoeksgroepen bezig met het ontwikkelen van software-paketten die het ontwerp en de analyse van termherschrijfsystemen ondersteunen. De algoritmen in deze software-systemen zijn vanzelfsprekend gebaseerd op theorie over termherschrijving. Wij hebben uitsluitend theorie behandeld die zijn weg naar deze algoritmen al gevonden heeft.

Binnen het fundamentele onderzoek betreffende software engineering neemt de hiervoor genoemde ontwikkeling van software ten behoeve van de analyse van termherschrijfsystemen een niet onbelangrijke plaats in. Voor het beoefenen van dit deel van de experimentele informatica bevat dit boek de noodzakelijke theoretische basis.

Wij bedanken Sylvia van Egmond en Frans Heeman voor het zeer grondig doorlezen van eerdere versies van de tekst. Hun commentaar heeft vele onnauwkeurigheden aan het licht gebracht en tevens de layout aanmerkelijk verbeterd. Ook zijn wij dank verschuldigd aan Roel de Vrijer en Hans Weigand voor het vinden van fouten en voorstellen tot verbeteringen in eerdere versies van de tekst.

BibTeX Entry

@book{THS89,
 author    = "Jan A. Bergstra and Jan Willem Klop and Aart Middeldorp",
 title     = "Termherschrijfsystemen",
 series    = "Programmatuurkunde",
 isbn      = "90-267-1356-8",
 publisher = "Kluwer Bedrijfswetenschappen",
 address   = "Deventer",
 note      = "In Dutch.",
 year      = 1989
}