Vrije Universiteit Amsterdam

Algoritmische termherschrijfsystemen


* Startdatum: 25-03-2010


* Tijd: 15.45


* Locatie: Aula


* Titel: Algoritmische termherschrijfsystemen


* Spreker: A. Isihara


* Promotor: prof.dr. J.W. Klop


* Onderdeel: Faculteit der Exacte Wetenschappen


* Wetenschapsgebied: Exacte wetenschappen


* Evenementtype: Promotie

Ariya Isihara bundelt voor het eerst de aspecten voor algoritmische termherschrijfsystemen, inductief voor eindige specificaties en coinductief voor oneindige specificaties, in een overkoepelend raamwerk. Toepassingen zijn pas op lange termijn te voorzien voornamelijk in vooruitgang van functionele programmeertalen.

In de jaren dertig van de vorige eeuw werden twee logische systemen ontdekt door de pioniers Gdel, Church, Kleene en Turing, die de basis legden voor het begrip 'berekenbaar' en het begrip 'informatie'. Dit waren de lambda calculus (LC) en de Combinatorische Logica (CL). Deze formele systemen leggen vast hoe `termen' in stappen getransformeerd kunnen worden, met het doel te komen tot een zogenaamde 'normaalvorm', een term die geen verder transformaties toelaat, een soort eindantwoord. In plaats van 'transformeren' zeggen we ook reduceren of herschrijven. LC en CL waren daarmee de eerste belangrijke termherschrijfsystemen, die het beginpunt waren van de informatica.

Later hebben die twee systemen de inspiratie gevormd voor de moderne functionele programmeertalen, en ook voor de theorie van 'algebraïsche specificaties'. Vanaf de jaren vijftig werden meer algemene termherschrijfsystemen bestudeerd, waarin ook patroonherkenning optreedt; de zogenaamde termherschrijfsystemen. Deze systemen zijn meer expressief dan LC en CL. Tot de jaren negentig bestudeerde men de eindige theorie van het termherschrijven; termen zijn daarbij eindige objecten, en herschrijfrijen zijn ook eindig. Het sleutelwoord is hier `inductie'. Sindsdien werd de aandacht gericht op oneindige termen en oneindige herschrijfrijen. Hierbij is het sleutelwoord `coinductief'.
© Copyright Vrije Universiteit Amsterdam