Next: Modell_3 Up: Unifikation Previous: Modell_1

Modell_2

Prinzipiell bleibt die Unifikation aus Modell_1erhalten. Es wird lediglich der Suchraum bei der Unifikation von Sorten auf die sortbase eingeschr"ankt. (Die Unifikation einer Sorte mit einer Dom"ane mu"s nicht angepa"st werden, da sie auf die Unifkation mit einer Konstanten zur"uckgreift.)


(defun sortbase-individualsp (const sort)
  (let ((res (and-process  (list (list 'constant-in-sort const sort))
                           '((bottom))
                           (list *rfi-sortbase*)
                           1
                           'once)))
       (ultimate-instant (un-inst (car res)) (cadr res))))


(defun sortbase-individualsp (sort1 sort2)
  (let ((res (and-process (list (list 'greatest-lower-bound sort1 sort2))
                          '((bottom))
                          (list *rfi-sortbase*)
                          1
                          'once)))
       (cadr (ultimate-instant (un-inst (car res)) (cadr res)))))


Harold Boley & Victoria Hall (hall@dfki.uni-kl.de)