Next: Modell_1 Up: Unifikation Previous: Unifikation

Unifikation mit ,,:``-Notation f"ur getypte Variablen

Prinzipiell ist die Unifikation aller Modelle gleich. Sie unterscheidet sich nur in den F"allen in denen Sorten auftreten. Deshalb werden nur die Funktionen dom-intersection, sortbase-individualsp und sortbase-glb.


(defun typ-t (x) (and (consp x) (eq 'typ (car x))))
(defun typ-tt (x) (and (typ-t x) (= 2 (length x))))

(defun typed-expr2bnd (term)         ; (expr1 : expr2) -> (bnd expr1 expr2)
  (cond ((typed-expr-t term)
         (mk-bnd (typed-expr-term term) (typed-expr-type term)))
        (t term)))


(defun unify
       (x y environment)

  (let ((x (typed-expr2bnd (ultimate-assoc x environment)))    ; typed-expr2bnd
        (y (typed-expr2bnd (ultimate-assoc y environment))))   ; see above

    (cond ((or (bnd-t x) (bnd-t y))
           (unify-bnd (un-bnd x)
                      (un-bnd y)
                      (variable-if-bnd x)
                      (variable-if-bnd y)
                      environment))
          ((equal x y) environment)
          ((or (anonymous-p x)
               (anonymous-p y))
           environment)
          ((vari-t x) (cons (list x y) environment))
          ((vari-t y) (cons (list y x) environment))
          ((and (dom-t x) (exc-t y)) (and (dom-exc x y) environment))
          ((and (exc-t x) (dom-t y)) (and (dom-exc y x) environment))
          ((and (dom-t x) (dom-t y)) (and (dom-intersection x y) environment))
          ((and (exc-t x) (exc-t y)) environment)

          ((and (dom-t x) (typ-t y)) (and (dom-in-sort x (s-type y))
                                          environment))
          ((and (typ-t x) (dom-t y)) (and (dom-in-sort y (s-type x))
                                          environment))

          ((dom-t x) (and (member y (cdr x) :test #'equal) environment))
          ((dom-t y) (and (member x (cdr y) :test #'equal) environment))
          ((exc-t x) (and (not (member y (cdr x) :test #'equal)) environment))
          ((exc-t y) (and (not (member x (cdr y) :test #'equal)) environment))

          ((and (typ-t x) (atom y))
               (and (sortbase-individualsp y (s-type x)) environment))
          ((and (atom x) (typ-t y))
               (and (sortbase-individualsp x (s-type y)) environment))
          ((and (typ-t x) (typ-t y))
               (and (mk-type (sortbase-glb  (s-type x) (s-type y)))
                environment))

          ((or (atom x) (atom y)) nil)
          (t
           (let ((new-environment (unify (car x)
                                         (car y)
                                         environment)))
             (and new-environment
                  (unify-args (cdr x) (cdr y) new-environment))))))))

(defun s-type (arg) (and (typ-t arg) (cadr arg)))

(defun mk-type (sort-name)
  (when sort-name
        (and (atom sort-name) (list 'typ sort-name))))



(defun unify-bnd (x y xvar yvar environment)
  (cond ((and (dom-t x) (exc-t y))
         (let ((differ (dom-exc x y)))
           (and differ (unify-bnd-env differ xvar yvar environment))))
        ((and (exc-t x) (dom-t y))
         (let ((differ (dom-exc y x)))
           (and differ (unify-bnd-env differ xvar yvar environment))))
        ((and (dom-t x) (dom-t y))
         (let ((inter (dom-intersection x y)))
           (and inter (unify-bnd-env inter xvar yvar environment))))
        ((and (exc-t x) (exc-t y))
         (unify-bnd-env (exc-union x y) xvar yvar environment))

        ((and (typ-t x) (dom-t y))
         (let ((sort-dom (dom-in-sort y (s-type x))))
              (and sort-dom (unify-bnd-env sort-dom xvar yvar environment))))
        ((and (dom-t x) (typ-t y))
         (let ((sort-dom (dom-in-sort x (s-type y))))
              (and sort-dom (unify-bnd-env sort-dom xvar yvar environment))))

        ((and (dom-t x) (not (vari-t y)))
         (and (member y (cdr x) :test #'equal)
              (unify-bnd-env y xvar yvar environment)))
        ((and (dom-t y) (not (vari-t x)))
         (and (member x (cdr y) :test #'equal)
              (unify-bnd-env x xvar yvar environment)))
        ((and (exc-t x) (not (vari-t y)))
         (and (not (member y (cdr x) :test #'equal))
              (unify-bnd-env y xvar yvar environment)))
        ((and (exc-t y) (not (vari-t x)))
         (and (not (member x (cdr y) :test #'equal))
              (unify-bnd-env x xvar yvar environment)))

        ((and (typ-t x) (typ-t y))
         (let ((sort-sort (mk-type (sortbase-glb (s-type x) (s-type y)))))
              (and sort-sort (unify-bnd-env sort-sort xvar yvar environment))))
        ((and (typ-t x) (not (vari-t y)))
         (and (sortbase-individualsp y (s-type x))
              (unify-bnd-env y xvar yvar environment)))
        ((and (typ-t y) (not (vari-t x)))
         (and (sortbase-individualsp x (s-type y))
              (unify-bnd-env x xvar yvar environment)))

        (t (let ((new (unify x y environment)))
             (and new (unify-bnd-env (if (vari-t x) x y) xvar yvar new))))
))


(defun ultimate-assoc
       (x environment)
  (cond ((vari-t x)
         (let ((binding (assoc x environment :test #'equal)))
           (cond ((null binding) x)
                 ((dom-t (cadr binding)) (mk-bnd x (cadr binding)))
                 ((exc-t (cadr binding)) (mk-bnd x (cadr binding)))

                 ((typ-t (cadr binding)) (mk-bnd x (cadr binding)))

                 (t (ultimate-assoc (cadr binding)
                                    environment)))))
        (t x)))





(defun ultimate-instant
       (x environment)
 (catch :bndclash    ; thrown at directly from (recursive) ultimate-instant-rec
  (cond ((bnd-t x)
         (let ((bndnew (unify (cadr x) (caddr x) environment)))
              (cond (bndnew (ultimate-instant-rec (cadr x) bndnew))
                    (t 'unknown))))

        ((typed-expr-t x)  ; still special treatment of (expr1 : expr2)
         (let ((bndnew (unify (car x) (caddr x) environment)))
              (cond (bndnew (ultimate-instant-rec (car x) bndnew))
                    (t 'unknown))))

        (t (ultimate-instant-rec x environment)))))



(defun ultimate-instant-rec ; could pair instantiated term with new environment
       (x environment)    ; for bnd-bnd composition, intermediate instantiation
  (cond ((vari-t x)                                     ; and throw elimination
         (let ((binding (assoc x environment :test #'equal)))
           (cond ((null binding) x)
                 (t (ultimate-instant-rec (cadr binding)
                                          environment)))))
        ((atom x) x)
        ((bar-t x)                                 ;  (cddr x) should be nil
         (let ((barinst (ultimate-instant-rec (cadr x) environment)))
              (cond ((tup-t barinst) (cdr barinst))
                    (t (list (car x) barinst)))))  ;  (car x) is "|"
        ((bnd-t (car x))
         (let ((bndnew (unify (cadr (car x)) (caddr (car x)) environment)))
              (cond (bndnew (cons (ultimate-instant-rec (cadr (car x)) bndnew)
                                  (ultimate-instant-rec (cdr x) bndnew)))
                    (t (throw :bndclash 'unknown)))))  ; escape from cons nest

        ((typed-expr-t (car x))  ; still special treatment of (expr1 : expr2)
         (let ((bndnew (unify (car (car x)) (caddr (car x)) environment)))
              (cond (bndnew (cons (ultimate-instant-rec (car (car x)) bndnew)
                                  (ultimate-instant-rec (cdr x) bndnew)))
                    (t (throw :bndclash 'unknown)))))  ; escape from cons nest

        (t
         (cons (ultimate-instant-rec (car x) environment)
               (ultimate-instant-rec (cdr x) environment)))))


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