Insbesondere soll die transitive Hülle einer solchen Relation berechenbar sein, denn wir möchten damit Nachfolgermengen bezüglich eines Term-Ersetzungs-Systems (TRS) beschreiben oder doch wenigstens approximieren.
Dauchet, Tison, Heuillard und Lescanne definierten dafür 1987 Ground Tree Transducer (GTTs) und zeigten damit die Entscheidbarkeit der Konfluenz von Grund-TRS. Seitdem haben verschiedene Autoren mit ähnlichen Ansätzen Approximations-Resultate für einige Klassen von TRS gewonnen.
Im Vortrag zeige ich zunächst zwei naive Ansätze, und erläutere dann GTTs und ihre Vorteile.
Schließlich diskutieren wir, ob und wie solche Methoden bei der Analyse von funktionalen Programmen von Nutzen sind. Wir können ja zunächst nur Funktionen erster Ordnung behandeln, und diese auch nur approximativ.
Literatur:
Abschnitt "Automata and n-ary Relations" aus: H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D. Lugiez and S. Tison and M. Tommasi: Tree Automata Techniques and Applications, http://www.grappa.univ-lille3.fr/tata/