Wolfram Kahl
Herbert Utz Verlag, München, Reihe Informatik, ISBN 3-931327-60-4, 1996, zugleich Dissertation an der Fakultät für Informatik der Universität der Bundeswehr München, Dezember 1995
1. Gutachter: Prof. Dr. Gunther Schmidt
2. Gutachter: Prof. Dr. Helmut Schwichtenberg
(.bib)
This thesis presents a first algebraic approach to term graph rewriting encompassing the treatment of bound variables. Building on a novel definition of term graphs with primitive notions of variable binding and variable identity, we present a concept of homomorphism avoiding ``capture of variables'' and catering for multiple instances of metavariables. Rewriting of these term graphs within the algebraic approach requires a new extension that is interesting in itself, the fibered approach to rewriting. As one result we obtain the first algebraic characterisation of graph reduction. Summing up, we have extended the algebraic approach to term graph rewriting, that so far only covered conventional term rewriting systems, to the expressive power of combinatory reduction systems and even slightly more general second-order rewriting systems. Thus we lay a theoretical foundation for implementations of functional programming languages, program transformation systems and other symbolic computation systems.
Most proofs can be found in [Kahl-1995a] zu finden.
This work is the foundation for the termgraph programming system
Diese Dissertation präsentiert einen ersten algebraischen Ansatz zu Termgraphersetzungssystemen unter Berücksichtigung gebundener Variablen.
Aufbauend auf eine neuartige Definition von Termgraphen, die Variablenbindung und Variablenidentität als primitive Konzepte einschließt und mehrstellige Metavariable zuläßt, werden zunächst Homomorphismen definiert, die ``Einfangen gebundener Variablen'' verhindern und für Entsprechungen zwischen den Bildern mehrfacher Instanzen von Metavariablen sorgen. Um einen diesen Termgraphen angemessenen algebraischen Ersetzungsbegriff finden zu können, wird der algebraische Ersetzungsansatz um eine neue Variante bereichert, den ``fibrierten Ansatz'', der auch um seiner selbst willen Interesse verdient. Ein bemerkenswertes Ergebnis ist die erste algebraische Charakterisierung der Graphreduktion.
Insgesamt wird die Ausdruckskraft des algebraischen Termgraphersetzungsansatzes, die bisher nur konventionelle Termersetzungssysteme umfaßte, so erweitert, daß auch die ``Combinatory Reduction Systems'' von Klop, die den Lambda-Kalkü einschließen, sowie noch allgemeinere Ersetzungssysteme zweiter Stufe behandelt werden können, und zwar sogar auf zyklischen Termgraphen. Damit wird eine theoretische Fundierung für Implementierungen von funktionalen Programmiersprachen, Programmtransformationssystemen und anderen Symbolmanipulationssystemen bereitgestellt.
Ein Großteil der Beweise ist in [Kahl-1995a] zu finden.