Options
1996
Diploma Thesis
Titel
Grundreduzierbarkeitstests und ihre Anwendungen in der Programmsynthese
Abstract
Der erste Teil der Arbeit besch=E4ftigt sich mit der Frage, welche Ver=E4nderungen an einem Vervollst=E4ndiger (insbesondere einem Unfailing-Vervollst=E4ndiger) vorgenommen werden m=FCssen, um ihn als= Werkzeug zur Programmsynthese nutzen zu k=F6nnen. Dabei wird unter Programmsynthese= der Proze=DF verstanden, der eine Menge von Gleichungen so in ein Regelsystem transformiert, da=DF s=E4mtliche zu definierenden Funktionssymbole vollst=E4ndig definiert sind. Als wichtigste Ver=E4nderungen werden identifiziert: die zielorientierte Auswahl kritischer Paare, das Erkennen des Endes der Synthese und die Extraktion eines Programms. Kernpunkt all dieser Erweiterungen ist ein Verfahren zum Test der Konvertierbarkeit. Dabei erweisen sich Verfahren,= die Testmengen verwenden, als besonders geeignet. Danach zeige ich, wie man damit die vorgeschlagenen Erweiterungen durchf=FChren kann. Dabei= abstrahiere ich jedoch von einem konkreten Verfahren. Ein Problem dieses Ansatzes zur Programmsynthese ist es, den Erhalt der Grundkonfluenz zu garantieren,= daher gehe ich auch darauf ein, wie man dieses Problem behandeln kann. Da der Test auf Konvertierbarkeit ein Spezialfall des Grundreduzierbarkeitstests ist, besch=E4ftige ich mich im zweiten Teil der Arbeit damit, die Grundreduzierbarkeit bzgl. linearer Regelsysteme zu testen. Ausgehend von den Arbeiten von Kapur, Narendran und Zhang ([KNZ91]) sowie B=FCndgen ([B=FCn91]) zeige ich, wie man die Vorteile beider Ans=E4tze in einem neuen Verfahren vereinigen kann. Im Unterschied zu anderen in der Literatur beschriebenen Verfahren habe ich= Wert darauf gelegt, da=DF das Verfahren bei schrittweiser Hinzuf=FCgung von= Regeln (inkrementelles Verfahren) ebenfalls effizient arbeitet. Im dritten Teil der Arbeit erweitere ich dieses Verfahren auf nichtlineare Regelsysteme. Im Gegensatz zu den in der Literatur beschriebenen Ans=E4tzen= , die auch praktisch einsetzbar sind, lasse ich zu, da=DF die Signatur= mehrere Sorten enth=E4lt. Einige Ideen f= FCr diese Erweiterung wurden den Ans=E4tze= n von Kounalis ([Kou90] bzw. [Kou92]), Hofbauer und Huber ([HH92a]) sowie Comon ([Com86a]) entnommen. Die Korrektheit dieses Ansatzes wird bewiesen und es werden Vorschl=E4ge gemacht, wie er zu einem Algorithmus erweitert werden kann. Dabei gehe ich auf die auftretenden Probleme ein und zeige L=F6sungsm=F6glichkeiten auf. Erg=E4nzt werden diese Verfahren sowohl durch M=F6glichkeiten zur= Optimierung der Generierung der Testmengen (beispielsweise im Kontext von Konvertierbarkeitstests), als auch durch Vorschl=E4ge zur Verkleinerung der Testmengen, was die Effizienz von Grundreduzierbarkeitstests wesentlich steigert. Diese Optimierungen sind fundamentaler Natur und lassen sich prinzipiell auch mit anderen in der Literatur beschriebenen Verfahren kombinieren.
ThesisNote
Kaiserslautern, Univ., Dipl.-Arb., 1996