Vorlesung: Praxis der Funktionalen Programmierung | Index

Abbrechende Berechnungen (Unifizieren)

Wir benutzen Bäume, um Terme darzustellen, die auch Variablen enthalten dürfen.
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)

Matching

Wenn nur im ersten Argument Variablen stehen, im zweiten keine, dann heißt die Aufgabe des Unifizierens matching. Anwendung: feststellen, ob und wie eine Term-Ersetzungs-Regel paßt.

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.

Höherer Ordnung

Bis jetzt war alles erster Ordnung, d. h. die Variablen bezeichneten Terme (Bäume). Beim Unifizieren zweiter Ordnung bezeichen Variablen Funktionen Term -> Term. D. h. die Variablen stellen wir uns als Funktionssymbole (mit Argumenten!) vor, die überall in den Bäumen stehen können. (Entsprechend höhere Ordnungen, ein Symbol dritter Ordnung hat als Argument(e) Symbole zweiter Ordnung.)

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?

Baumgleichungen

Man kann das Unifizieren zweiter Ordnung so einschränken: man erlaubt nicht beliebige Funktionen (als Werte der zu belegenden Variablen), sondern nur Kontexte (Bäume mit markierten Blättern). Durch solches Einsetzen wird der Baum also immer größer. (Eine "beliebige" Funktion könnte sich auch Teilbäume ansehen oder teilweise löschen. Hier darf nur ein Kontext eingeschoben werden, und auch ohne die Argumente des Funktionssymbols "auszuwerten".)

Während das volle Unifizieren unentscheidbar ist, ist die Frage nach der Lösbarkeit solcher Baumgleichungen offen. (TODO: Link einfügen) Diplomarbeit?


best viewed with any browser


http://www.informatik.uni-leipzig.de/~joe/ mailto:joe@informatik.uni-leipzig.de