Termherschijfsystemen / Term Rewriting Systems
Downloads
Termination Tools
Referenties
[Cas05] Pierre Castéran, Omega Enriched Coq (PDF), Draft version, June 14, 2005.
In mijn bachelorscriptie presenteer ik een termherschrijfsysteem voor het rekenen met ordinaal getallen tot epsilon-0 (ε0). Dit termherschrijfsysteem is gebaseerd op de rekenregels van Pierre Castéran [Cas05]. In de scriptie wordt een afbeelding gedefinieerd voor het omzetten van ordinaal getallen naar eindige bomen en eindige termen. Er worden herschrijfregels gedefinieerd voor het rekenen (optellen en vermenigvuldigen) van deze termen representerend een ordinaal getal. Er wordt bewezen dat de optelling correct is (onder het voorbehoud dat de regels van Castéran correct zijn). Om verdere overtuiging te geven worden enkele voorbeelden van Rubin en Simmons uitgewerkt. Als laatste wordt er bewezen dat het systeem confluent (CR) en sterk normaliserend (SN) is.
Deze scriptie heb ik geschreven onder de supervisie van prof. dr. Jan Willem Klop en dr. Roel de Vrijer.
IJsbrand Oudshoorn, Rekenen met ordinalen in een termherschrijfsysteem (PDF), bachelorscriptie, Vrije Universiteit Amsterdam, 31 augustus 2005.
IJsbrand Oudshoorn, Rekenen met ordinalen in een termherschrijfsysteem (PDF), presentatie bachelorscriptie, Vrije Universiteit Amsterdam, 31 augustus 2005.
Jan Willem Klop, IJsbrand Oudshoorn, Ordinal arithmetic via infinitary term rewriting, Process Algebra Meetings (PAM), CWI Amsterdam, 30 november 2005.