module Term where import Form import Bild import Sort data Term = Leaf | Variable { name :: Int } | Node { left :: Term, right :: Term } deriving Show instance Eq Term where Leaf == Leaf = True Variable { name = v } == Variable { name = w } = v == w Node { left = l, right = r } == Node { left = ll, right = rr } = (l == ll) && (r == rr) _ == _ = False tfold :: b -> (Int -> b) -> (b -> b -> b) -> (Term -> b) tfold leaf var node (Leaf) = leaf tfold leaf var node (Variable { name = n }) = var n tfold leaf var node (Node { left = l, right = r }) = node (tfold leaf var node l) (tfold leaf var node r) instance Form Term where form = tfold ( kreis 0.5 ) ( form ) ( \ l r -> krone (kreis 0.5) [ l, r ] ) variables :: Term -> [ Int ] variables = unique . tfold [] ( \ n -> [n] ) (++)Wir können substituieren, das heißt, eine Abbildung von Variablen auf Terme anwenden.
module Subst where import Term type Subst = [ (Int, Term) ] apply :: Subst -> Term -> Term apply subst Leaf = Leaf apply subst ( Variable { name = n } ) = case [ w | (v, w) <- subst, v == n ] of [ ] -> Variable { name = n } -- bleibt stehen [ w ] -> w -- wird ersetzt _ -> error $ "Variable mehrfach gebunden " ++ show substNun fragen wir uns, ob zwei gegebene Terme t1 und t2 unifizierbar sind, d. h. ob es ein s :: Subst gibt, so daß apply s t1 = apply s t2. Wir wissen, daß es in solch einem Fall sogar (bis auf Umbenennungen) genau einen allgemeinsten Unifikator s gibt.
Um den zu finden, verwenden wir einen naiven Algorithmus: wir unifizieren von links nach rechts und wenden jeweils die festgelegten Substitutionen sofort im noch zu unifizierenden Teil an. Natürlich gibt es Paare von nicht unifizierbaren Termen, deswegen ist der Ergebnistyp Maybe Subst.
Wieder (vergleiche das Zählen im Baum) geht es um Nacheinanderausführung von Rechnungen (erst linke Teilbäume, dann rechte unifizieren). Diese Kopplung geschieht durch das bind in der Monade Maybe: Wenn die Rechung erfolglos ist, setzen wir sie nicht fort; sonst tun wir es.
instance Functor Maybe where fmap f Nothing = Nothing; fmap f (Just x) = Just (f x) instance Monad Maybe where return x = Just x Nothing >>= f = Nothing; Just x >>= f = f xJetzt benutzen wir die do-Notation (eigentlich nur in der allerletzten Klausel des folgenden Programms).
module Unify where import Term import Subst unify :: Term -> Term -> Maybe Subst unify t1 t2 = uni [] t1 t2 uni :: Subst -> Term -> Term -> Maybe Subst -- identische Terme gehen immer uni current l r | l == r = Just current -- eine Variable wird gebunden (beachte n /= r) uni current (Variable { name = n }) r = if n `elem` variables r -- der berühmte occurs-check then Nothing else return $ (n, r) : current uni current l r @ (Variable { name = n }) = uni current r l -- hier ist r keine Variable uni current Leaf r = if r == Leaf then return current else Nothing uni current l r @ Leaf = uni current r l -- jetzt sind beides Verwzeigungen uni current t1 t2 = do lsub <- uni current (left t1) (left t2) rsub <- uni lsub (apply lsub (right t1)) (apply lsub (right t2)) return rsubAufgaben (von leicht bis sehr schwer)
Wir können leicht einen Matching-Algorithmus aufschreiben, indem wir den vom Unifizieren nehmen und alle Fälle löschen, die sich mit Variablen im zweiten Argument beschäftigen.
Es stellt sich heraus, daß das viel schwieriger ist, bereits Unifikation zweiter Ordnung ist unentscheidbar (durch Reduktion vom Postschen Korrespondenzproblem).
Bei einigen (an sich wünschenswerten) Erweiterungen des Haskell-Typ- und Konstruktor-Klassen-Systems muß man das berücksichtigen. Erlaubt man zuviel, muß der Compiler unter Umständen Unifikatoren zweiter Ordnung (von Typausdrücken) bestimmen, und das geht eben nur mit passenden Einschränkungen.
Die Entscheidbarkeit vom Matching verschiedener Ordnung ist Gegenstand aktueller Forschungen (Siehe RTALOOP TODO: Link). Sie ist bis vierter Ordnung entscheidbar, mit Baum-Automaten, und darüber ist es offen. Diplomarbeit gefällig?
Während das volle Unifizieren unentscheidbar ist, ist die Frage nach der Lösbarkeit solcher Baumgleichungen offen. (TODO: Link einfügen) Diplomarbeit?