Next: Tools zur Pr;;ufung Up: Modell_3 Previous: Modell_3

Vorcompilation



(defvar *rfi-sortbase*        nil  "taxonomic knowledge ")

;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

(defun compile-sortbase (sortbase)
  (setq *subsumes-individuals* (and (compile1-sortbase sortbase)
                               (classify-subsumes* (classify-sortbase)))))


;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

(defvar *subsumes-individuals* nil)

;************************************************************************
; Explicit relations: subsumes and individuals
;************************************************************************

;The structure of *subsumes-individuals* after the first compilation step
;(compile1-sortbase) :
;( (sort1 (subsumes subsort11 subsort12 ...) (individuals ind11 ind12 ...))
;  (sort2 (subsumes subsort21 subsort22 ...) (individuals ind21 ind22 ...))
;  (sort3 (subsumes subsort31 subsort32 ...) (individuals ind31 ind32 ...))
;               ...
;  (sortn (subsumes subsortn1 subsortn2 ...) (individuals indn1 indn2 ...))
;)
;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *


(defun compile1-sortbase (sortbase)
  (cond (sortbase
         (let ((clause (car sortbase)))
              (cond ((subsumes-t clause)
                     (let ((sort (cadadr clause))
                           (subsort (caddr (cadr clause))))
                          (add-sort-and-subsort sort subsort)))
                    ((horn-sort-rel-t clause)
                     (let ((sort (caadr clause))
                           (subsort (caaddr clause)))
                          (add-sort-and-subsort sort subsort)))
                    ((individual-assignment-t clause)
                     (let ((sort (caadr clause))
                           (individual (cadadr clause)))
                          (cond ((dom-t individual)
                                 (mapcar #'(lambda (dom-individual)
                                                   (add-sort-and-individual
                                                    sort dom-individual))
                                         (cdr individual)))
                                (t ;individual is a constant
                                   (add-sort-and-individual sort
                                                          individual)))))))
         (compile1-sortbase (cdr sortbase)))
        (t *subsumes-individuals*)))

;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

(defun add-sort-and-subsort (sort subsort)
  (cond ((null *subsumes-individuals*)
         (initial-subsumes-individuals1 sort subsort))
        ((member-tree sort *subsumes-individuals*)
         (assert-sub sort subsort))
        (t (assert-sort1 sort subsort))))


(defun add-sort-and-individual (sort individual)
  (cond ((null *subsumes-individuals*)
         (initial-subsumes-individuals2 sort individual))
        ((member-tree sort *subsumes-individuals*)
         (assert-individuals sort individual))
        (t (assert-sort2 sort individual))))

(defun initial-subsumes-individuals1 (sort subsort)
  (setq *subsumes-individuals*
        (list (list sort (list 'subsumes subsort) (list 'individuals))
              (list subsort (list 'subsumes) (list 'individuals)))))

(defun initial-subsumes-individuals2 (sort individual)
  (setq *subsumes-individuals*
        (list (list sort (list 'subsumes) (list 'individuals individual)))))


;Asserts a sort in the *subsumes-individuals* with the subsorts of the
;`Subsumes-List' and asserts the subsorts in the *subsumes-individuals*,
;if not existent yet
(defun assert-sort1 (sort subsort)
  (setq *subsumes-individuals*
        (append *subsumes-individuals*
                (list
                 (list sort (list 'subsumes subsort) (list 'individuals)))))
  (cond ((member-tree subsort *subsumes-individuals*) t)
        (t (assert-subsort subsort))))

;Asserts a sort in the *subsumes-individuals* with the individual in the
;`individual-list'
(defun assert-sort2 (sort individual)
  (setq *subsumes-individuals*
        (append *subsumes-individuals*
                (list
                 (list sort (list 'subsumes) (list 'individuals individual))))))


;Asserts a subsort in the `subsumes-list', if not existent yet and
;asserts this subsort in the *subsumes-individuals*.
(defun assert-sub (sort subsort)
  (setq *subsumes-individuals*
        (mapcar #'(lambda (list)
                          (cond ((and (equal sort (car list))
                                      (not (member subsort (cadr list))))
                                 (list (car list)
                                       (append (cadr list) (list subsort))
                                       (caddr list)))
                                (t list)))
                *subsumes-individuals*))
  (cond ((member-tree subsort *subsumes-individuals*) t)
        (t (assert-subsort subsort))))

;Assert a subsort in the *subsumes-individuals*
(defun assert-subsort (subsort)
  (setq *subsumes-individuals*
        (append *subsumes-individuals*
                (list (list subsort
                            (list 'subsumes)
                            (list 'individuals))))))



;Assert an individual of the sort in the `individual-list'
(defun assert-individuals (sort individual)
  (setq *subsumes-individuals*
        (mapcar #'(lambda (list) (cond ((equal sort (car list))
                                        (list (car list)
                                              (cadr list)
                                              (append (caddr list)
                                                      (list individual))))
                                       (t list)))
                *subsumes-individuals*)))
;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
(defun horn-sort-rel-t (clause)
    (= (length clause) 3) )

(defun individual-assignment-t (clause)
  (= (length clause) 2))

(defun member-tree (sort subsumes-individuals)
  (and subsumes-individuals
       (if (equal sort (caar subsumes-individuals)) t
           (member-tree sort (cdr subsumes-individuals)))))

;************************************************************************
; Transitive closure: subsumes* and individuals*
;************************************************************************

(defun classify-sortbase ()
  ;1. Add to the *subsumes-individuals* the `subsumes*-list' with the
  ;   sorts of the `subsumes-list' and the `individual*-list'
  ;   with the individuals of the `individual-list'
  (setq *subsumes-individuals* (extend-sub-ind-list *subsumes-individuals*))

  ;2. Add all elements from the stratified list
  ;    a. `subsumes-list' is empty -> finished
  ;    b. `subsumes-list' is not empty ->
  ;         add all elements from the `subsumes-list'
  ;            (expand `subsumes*-list' with the `subsumes*-list'
  ;            (of each element and `individual*-list' analogue)
  (expand-sort-list (stratify-list *subsumes-individuals*)))


(defun extend-sub-ind-list (sub-ind-list)
  (mapcar #'(lambda (sort-list)
                    (append sort-list
                            (list (cons 'subsumes* (cons (car sort-list)
                                                        (cdadr sort-list)))
                                  (cons 'individuals* (cdaddr sort-list)))))
                    sub-ind-list))

;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
(defvar *stratified-list* nil)

(defun stratify-list (subsumes-list)
    (setq *stratified-list* (sort-depexpr (mk-subsumes-list subsumes-list))))

(defun mk-subsumes-list (sub-ind-list)
    (mapcar #'(lambda (x) (cons (car x) (cdadr x)))
                      sub-ind-list))


;* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
(defun expand-sort-list (stratified-list)
  (cond ((null stratified-list) *subsumes-individuals*)
        (t    (let ((sort (car stratified-list)))
                   (setq *subsumes-individuals*
                         (mapcar #'(lambda (sort-list)
                                           (cond ((sort-list-t sort-list sort)
                                                  (expand-sub*-ind* sort-list))
                                                 (t sort-list)))
                                 *subsumes-individuals*))
                   (expand-sort-list (cdr stratified-list))))))


(defun expand-sub*-ind* (sort-list)
  (let ((sort (car sort-list))
        (sub-list (get-sub-list sort-list))
        (ind-list (get-ind-list sort-list))
        (sub*-list (get-sub*-list sort-list))
        (ind*-list (get-ind*-list sort-list)))
       (list sort sub-list ind-list
             (expand-sub* sub*-list (cdr sub-list))
             (expand-ind* ind*-list (cdr sub-list)))))


(defun expand-sub* (sub*-list sub-list)
  (cond ((null sub-list) sub*-list)
        (t (expand-sub* (append-not-twice sub*-list
                                          (get-sub*-list
                                           (get-sort-list *subsumes-individuals*
                                                          (car sub-list))))
                        (cdr sub-list)))))

(defun expand-ind* (ind*-list sub-list)
  (cond ((null sub-list) ind*-list)
        (t (expand-ind* (append-not-twice ind*-list
                                          (get-ind*-list
                                           (get-sort-list *subsumes-individuals*
                                                          (car sub-list))))
                        (cdr sub-list)))))



(defun get-sort-list (sub-ind-list sort)
  (when sub-ind-list
        (let ((sort-list (car sub-ind-list)))
             (cond ((equal (car sort-list) sort) sort-list)
                   (t (get-sort-list (cdr sub-ind-list) sort))))))


(defun get-sub*-list (sort-list)   ; returned 'lists' start with sub/ind[*] tag
  (cadddr sort-list))

(defun get-ind*-list (sort-list)
  (car (last sort-list)))

(defun get-sub-list (sort-list)
  (cadr sort-list))

(defun get-ind-list (sort-list)
  (caddr sort-list))


(defun append-not-twice (sub*-list1 sub*-list2)
  (cond ((null sub*-list2) sub*-list1)
        (t (cond ((member (car sub*-list2) sub*-list1 :test 'equal)
                  (append-not-twice sub*-list1 (cdr sub*-list2)))
                 (t (append-not-twice (append  sub*-list1
                                               (list (car sub*-list2)))
                                      (cdr sub*-list2)))))))


(defun sort-list-t (sort-list sort)
  (equal (car sort-list) sort))


;*******************************************************************************


(defun classify-subsumes* (sub-ind-list)
  (mapcar #'(lambda (sort-list)
                    (let ((sort (car sort-list))
                          (sub-list (get-sub-list sort-list))
                          (ind-list (get-ind-list sort-list))
                          (sub*-list (get-sub*-list sort-list))
                          (ind*-list (get-ind*-list sort-list)))
                         (list sort sub-list ind-list
                               (sort-subsumes* sub*-list
                                               *stratified-list*)
                               ind*-list)))
          sub-ind-list))


(defun sort-subsumes* (a b)
    (sort (copy-list a) #'(lambda (y x) (member y (member x b)))))


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