Graphersetzung ist ein Turing-vollsta¨ndiges Berechnungsmodell, welches insbesondere in solchen Gebieten Verwendung findet, in denen Probleme durch Graphen modelliert werden ko¨nnen. Eine bekannte Anwendung ist die Ersetzung von Termgraphen in der funktionalen Programmierung. Die Frage nach der Terminierung ist ein wichtiger Punkt, da zum Beispiel eine Endlosschleife selten ein intendiertes Verhalten darstellt. Fu¨r Graphersetzungssysteme ist diese Frage im Allgemeinen jedoch unentscheidbar (vgl. [Plu98]). Die Idee der U¨ bersetzung von Graphersetzung in aussagenlogische Formeln wurde in [KKW10] eingefu¨hrt, in [Erm13] mit einem Ansatz zur induktiven Verifikation von HaskellProgrammen verbunden und wird hier im Sinne des Erkennens von Schleifen in Ableitungen mit einer Anwendung auf Haskell weiter vorangetrieben.
Definition 1 Ein Graphersetzungssystem GRS mit initialem Graphen G0 und Regelmenge P ohne knotenlo¨schende Regeln entha¨lt eine Schleife genau dann, wenn Graphen G; H + und ein injektiver Graphmorphismus g: G ! H existieren, so dass G0 =P) G =) H gilt. P In der SAT-Kodierung bleibt die Knotenmenge invariant, wobei Knotenaddition durch spezielle Markierungen umgesetzt wird. Dass ein Graph in einer Ableitung der La¨nge m > 0 isomorph zu einem Teilgraphen des letzten Graphen der Ableitung ist, wird kodiert durch: m 1 loop(m) = W W V edge(v; a; v0; k) ! edge(g(v); a; g(v0); m) , k=0 g2M(n;n) (v;a;v0)2E wobei M(n; n) die Menge aller Abbildungen zwischen den Knoten der invarianten Knotenmenge ist und Kanten in E aus zwei Knoten und einer Markierung bestehen. Das Erkennen einer Schleife in allen Ableitungen bis zu einer La¨nge k 2 N wird kodiert durch k loop det(G0; k) = W der(G0; m) ^ loop(m) ,
m=1 wobei der(G0; m) die aussagenlogische Kodierung einer Ableitung der La¨nge m beginnend in G0 gema¨ß [KKW10] ist. Der Zusammenhang zu Schleifen ist der folgende. Satz 2 GRS entha¨lt eine Schleife, falls es ein k gibt, so dass loop det(G0; k) erfu¨llbar ist. permute 1 2 x y !
Abbildung 1: Anwendung der Regel permute (links) fu¨hrt zu einer Schleife (rechts) Betrachten wir eine Funktion permute x y = permute y x zur Permutation von Argumenten, die links in Abbildung 1 als Termgraphersetzungsregel gegeben ist. Rechts in Abbildung 1 findet man eine Ableitung, beginnend beim Termgraphen von permute 0 1, in der die zweifache Anwendung von permute zu einer Schleife fu¨hrt. Eine erfu¨llende Belegung fu¨r die Teilformel der(permute 0 1; 2) ^ loop(2) erkennt die Schleife.
[Erm13]
Marcus Ermler. Towards a Verification Framework for Haskell by Combining Graph Transformation Units and SAT Solving. Bericht 1306, Christian-Albrechts-Universita¨t zu Kiel, September 2013. Michael Hanus und Ricardo Rocha, Hrsg., Seiten 138-152. [Kre78] [Plu98]