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 subst
Nun 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 x
Jetzt 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 rsub
Aufgaben (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?