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.
Ich schlage eine Klasse von Relationen MDGTT vor, die in gewissem Sinne dual zu GTT ist. Sie erbt viele der GTT-Eigenschaften. Auch Beweisideen lassen sich übertragen, benötigen aber Modifikationen.
An Beispielen zeige ich, wie sich GTTs und DGTTs bei der Approximation von Nachfolgermengen ergänzen.
this page is best viewed with any browser