Next: Modell_2 Up: Unifikation Previous: Unifikation mit,:``-Notation

Modell_1

Die Unifikation von Dom"anen und Sorten wird auf mehrere Konstanten-Sorten-Unifikationsschritte reduziert. Eine solche Konstanten-Sorten-Unifikation ruft die RELFUN-Relation constant-in-sort auf. Ebenso wird bei der Sorten-Sorten-Unifikation eine RELFUN-Relation greatest-lower-bound benutzt.

(defun dom-in-sort (dom sort)
  (and dom
       (mk-dom (remove nil (const-list-in-sort (cdr dom) sort)))))

(defun const-list-in-sort (const_list sort)
  (cond ((null const_list) nil)
(t (cons (sortbase-individualsp (car const_list) sort)
                 (const-list-in-sort (cdr const_list) sort)))))


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


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

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