Next: UNSUBSUMES und RESUBSUMES Up: Modell_3 Previous: Vorcompilation

Tools zur Pr"ufung der Restriktionen



(defun all-sorts (sub-ind-list) ; select sorts from a subsumes-individuals list
  (mapcar #'(lambda (sort-list) (car sort-list)) sub-ind-list))

(defun combine-all-sorts (list1 list2) ; pair two lists
  (cond ((null list1) nil)
        ((null list2) (combine-all-sorts (cdr list1) (cddr list1)))
        (t (cons (list (car list1)
                       (car list2))
                 (combine-all-sorts list1 (cdr list2))))))

;**************************************************************************
; Check the taxonomy for completeness (intensional glb = extensional glb)
;**************************************************************************

(defun complete-taxonomy ()
  (complete-taxonomy1
   (combine-all-sorts (all-sorts *subsumes-individuals*)
                        (cdr (all-sorts *subsumes-individuals*)))))

(defun complete-taxonomy1 (comb-sort-list)
  (if  comb-sort-list
       (let ((sort1 (caar comb-sort-list))
             (sort2 (cadar comb-sort-list)))
            (cond ((int-ext-intersection-equal sort1 sort2)
                   (complete-taxonomy1 (cdr comb-sort-list)))
                  (t (rf-format "Taxonomy is not complete: ~a ~a ~%"
                                sort1 sort2))))
       t))

(defun int-ext-intersection-equal (sort1 sort2)
  (let ((int-intersection (intensional-intersection sort1 sort2))
        (ext-intersection (extensional-intersection sort1 sort2)))
       (cond ((null (set-difference
                     int-intersection
                     (cdr (get-ind*-list
                           (get-sort-list
                            *subsumes-individuals* ext-intersection)))))
              t)
             (t nil))))

(defun extensional-intersection (sort1 sort2)
  (sortbase-glb sort1 sort2))

(defun intensional-intersection (sort1 sort2)
  (intersection (cdr (get-ind*-list
                      (get-sort-list *subsumes-individuals* sort1)))
                (cdr (get-ind*-list
                      (get-sort-list *subsumes-individuals* sort2)))))

;**************************************************************************
; Check the taxonomy for uniqueness (i.e., there is at most one glb defined)
;**************************************************************************

(defun unique-glb ()
 (unique-glb1
  (combine-all-sorts (all-sorts *subsumes-individuals*)
                       (cdr (all-sorts *subsumes-individuals*)))))

(defun unique-glb1 (comb-sort-list)
  (if comb-sort-list
      (let ((sort1 (caar comb-sort-list))
            (sort2 (cadar comb-sort-list)))
           (cond ((<= (length (dyn-glb sort1 sort2)) 1)
                  (unique-glb1 (cdr comb-sort-list)))
                 (t   (rf-format "Taxonomy is not well defined: ~a ~a ~%"
                                 sort1 sort2))))
      t))

(defun dyn-glb (sort1 sort2)
  (remove-subsumed-clbs (clb sort1 sort2)))

(defun clb (sort1 sort2)
   (intersection (cdr (get-sub*-list
                       (get-sort-list *subsumes-individuals* sort1)))
                 (cdr (get-sub*-list
                       (get-sort-list *subsumes-individuals* sort2)))))

(defun remove-subsumed-clbs (clbs)
  (rsl clbs nil))

(defun rsl (list1 list2)
  (cond ((null list1) list2)
        (t (let ((clb (car list1))
                 (clb-rest (cdr list1)))
                (rsl (rsl1 clb clb-rest)
                     (cons clb (rsl1 clb list2)))))))

(defun rsl1 (clb list2)
  (cond ((null list2) nil)
        ((subsumes+ clb (car list2)) (rsl1 clb (cdr list2)))
        (t (cons (car list2) (rsl1 clb (cdr list2))))))

(defun subsumes+ (sort1 sort2)
  (member sort2 (get-sub*-list
                        (get-sort-list *subsumes-individuals* sort1))))


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