Kategorien von Termgraphen mit gebundenen Variablen

Wolfram Kahl

Technischer Bericht Nr. 9503, 191 pages
Fakultät für Informatik
Universität der Bundeswehr München
September 1997
(.bib, .ps.gz slightly reformatted)

Zusammenfassung

Mit dem Ziel einer Erweiterung der algebraischen Termgraphersetzung auf die Ausdruckskraft von ``Combinatory Reduction Systems'' führen wir zuerst eine neuartige Definition von Termgraphen ein, in der Variablenbindung und Variablenidentität primitive Konzepte sind, und die Metavariable mit Nachfolgern erlaubt. Nach der Diskussion von Identifizierung und Sharing in diesen Graphen definieren wir Intervalle und Abschnitte, die als Bilder von Metavariablen, insbesondere auch von solchen mit Nachfolgern, dienen können. Darauf aufbauend gelingt es uns, eine Hierarchie von strukturerhaltenden Abbildungen zwischen unseren Termgraphen zu errichten, die an ihrer Spitze einen Homomorphismenbegriff hat, der ``Einfangen von Variablen'' vermeidet und mehrfache Instanzen von Metavariablen angemessen berücksichtigt. Die verschiedenen Kategorien, die wir so erhalten, haben unterschiedliche Anwendungen, insbesondere in der Termgraphersetzung. Im Anhang präsentieren wir einen Überblick über einen neuartigen Ansatz zur algebraischen Termgraphersetzung (der in [Kahl-1996] ausführlich vorgestellt wird) zusammen mit den zwei wesentlichen Beweisen zur Durchführbarkeit der benötigten Konstuktionen.

Abstract

With the aim of extending algebraic term graph rewriting to the expressiveness of Combinatory Reduction Systems, we first introduce a novel definition of term graphs with primitive notions of variable binding and variable identity, and with metavariables with successors. After discussing identification and sharing in these graphs, we introduce intervals and segments to serve as images of metavariables, including those with successors. Building on this we are able to establish a hierarchy of structure-preserving mappings between our term graphs, including at its top a concept of homomorphism avoiding ``capture of variables'' and catering for multiple instances of metavariables. The individual categories this gives rise to have different uses, namely in term graph rewriting, and the appendix provides an overview over a novel approach to algebraic term graph rewriting (fully presented in [Kahl-1996]) together with the two crucial proofs concerning the viability of the constructions involved.


Wolfram Kahl --- 24 February 1999