;;; ============================================================================
;;; L"osungsvorschlag zum "Ubungsblatt 6, Aufgabe 1
;;; *** Most General Unifier ***
;;; 10.06.96 U. Reuther (reuther@informatik.uni-freiburg.de)
;;; ============================================================================
(in-package USER)



;;; ============================================================================
;;; Zum Warmwerden erstmal die Repr"asentationen der Pr"adikate vom "Ubungsblatt
;;; ============================================================================

(defvar *A1* '((P (? x) a)              (P b (? y))))

(defvar *A2* '((Q a)                    (Q (f (? x)))))

(defvar *A3* '((P (f (? y)))            (P (f (g (? z))))))

(defvar *A4* '((P (? x))                (Q (? x))))

(defvar *A5* '((P (? x) (f (? x)) a)    (P b (? y) (? x))))


;;; ============================================================================
;;; Die special-Variablen sind nur f"ur die Ausgabe mittels SHOW-MGU und zum
;;; "Aufheben" der Ergebnisse notwendig. *P* enth"alt die an mgu "ubergebenen 
;;; Pr"adikate in bereinigter Form, d.h. so umbenannt, da"s keine Variable in 
;;; mehreren vorkommt.
;;; *MGU* enth"alt den Unifikator 
;;; oder NIL, wenn alle Pr"adikate identisch sind (also auch keine Variablen!)
;;; oder :OCCUR-CHECK, wenn beim Unifizieren der occur check fehlschlug,
;;; oder :NO-VAR, wenn eine Unterschiedsmenge keine Variablen enthielt.
;;; *U* enth"alt im Erfolgsfall das unifizierte Pr"adikat.
;;; *DIFF* enth"alt die zuletzt bearbeitete Unterschiedsmenge bzw. NIL. *DIFF*
;;; ist interessant, wenn :OCCUR-CHECK oder :NO-VAR auftrat.
;;; Keine dieser Variablen m"usste f"ur den Programlauf ohne SHOW-MGU special
;;; sein.
(defvar *P*)
(defvar *MGU*)
(defvar *U*)
(defvar *DIFF*)
;;; ============================================================================

;;; ============================================================================
;;; Einige Hilfsfunktionen
;;; ============================================================================

;; Handelt es sich bei v um eine Variable ?
(defun is-var (v)
  (and (consp v) (eql (length v) 2) (eq (first v) '?)))

;; Wenn es sich bei v um eine Variable handelt, dann liefere das 
;; Variablensymbol  zur"uck, sonst NIL.
(defun get-varname (v)
  (if (is-var v) (second v)))

;; Baue aus einem Variablen "(? x)" und einem Term "t" eine Substitution. 
;; Liefert Liste (x  t). 
(defun new-substitution (var term)
  (if (is-var var)
      (list (get-varname var) term)
    :ERROR))

;; finde in einer Liste eine bel. Variable (die erste)
(defun find-var-in-difflist (difflist)
  (find-if 
   #'(lambda (term) (is-var term)) 
   difflist))

;; finde in einer Liste einen bel. Term, der eine Variable NICHT enth"alt
(defun find-term-in-difflist (var difflist)
  (find-if 
   #'(lambda (term) (not (occur-check-fails (get-varname var) term)))
   difflist))

;;; ============================================================================
;;; DO-REPLACE-VARNAMES <LISTE VON PRAEDIKATEN>
;; F"uhre REPLACE-VARNAMES auf allen Pr"adikaten in predlist aus
(defun do-replace-varnames (predlist)
  (let ((result nil))
    (dolist (x predlist result)
      (setq result (cons (replace-varnames x) result)))))
      
;;; ============================================================================
;;; REPLACE-VARNAMES <PRAEDIKAT>
;; Wenn Pr"adikate unifiziert werden sollen, d"urfen sie zu Beginn keine 
;; Variablensymbole gemeinsam haben. (Solche Pr"adikate waeren sonst im Skopus
;; *eines* Quantors gewesen...)
;; replace-varnames ersetzt alle Variablennamen durch ein eindeutiges Symbol.
(defun replace-varnames (pred)
  (let ((result pred))
    (dolist (x (remove-duplicates (find-variables result) :TEST #'equal) result)
      (setq result (substitute-var result x (new-varname))))))

;;; Neuen Variablensymbol erzeugen, das mit VAR_ beginnt
(defun new-varname ()
  (list '? (intern (gensym "VAR_"))))

;;; Finde alle Variablen und gib sie als Liste zur"uck
(defun find-variables (l)
  (cond 
   ((atom l)   ;; Atome sind keine Variablen, nix zu tun
    nil)
   ((is-var l) ;; 
    (list l))
   (T
    (append (find-variables (first l)) 
            (find-variables (rest l))))))


;;; ============================================================================
;;; GET-DIFF-LIST <LISTE VON TERMEN>
;; Finde eine Unterschiedsliste in den "ubergebenen Termen. Wenn es keinen 
;; Unterschied gibt, gib NIL zur"uck. 
(defun get-diff-list (terms)
  ;; Alle echten Duplikate entfernen
  (setq terms (remove-duplicates terms :test #'equal))
  
  (cond 
   ;; Wenn terms ein Element enth"alt, gibt es keine Unterschiede...
   ((null (rest terms))
    nil)
   ;; Dann die Duplikate bzgl. des Funktionssymbols und der Argumentenanzahl
   ;; entfernen mit top-equal (s.u.)   (nur so tun als ob...)
   ;; Wenn es noch mehr als einen Term gibt, dann ist das die Unterschiedsliste
   ((rest (remove-duplicates terms :test #'top-equal))
    terms)
   ;; Wenn es sich bei der Funktion um eine Konstante handelt, ist durch das
   ;; Entfernen der echten Duplikate die Unterschiedsmenge ebenfalls bereits 
   ;; bestimmt
   ((atom (first terms))
    terms)
   (T
    ;; F"uhre den Vergleich f"ur alle Argumente der Terme in terms durch.
    (let ((result))
      (dotimes (arg (1- (length (first terms))) result)
        (setq result 
          (get-diff-list (mapcar #'(lambda (x) (nth (1+ arg) x)) terms)))

        ;; Wenn result jetzt nicht NIL ist, wurden Unterschiede gefunden und
        ;; fertig
        (when result
          (return result)))))))
  
;; Stimmen das Funktionssymbol und die Argumentenanzahl zweier Terme/Pr"adikate
;; "uberein ?
(defun top-equal (a b)
  (cond 
   ((or (atom a) (atom b))
    (eql a b))
   ;; weder a noch b ist Atom
   (T 
    (and (eq (first a) (first b))
         (eql (length a) (length b))))))
             

;;; ============================================================================
;;; OCCUR-CHECK-FAILS <VARIABLENNAME> <TERM>
;; wenn die Variable z.B. "x" im Term z.B. "(f a (g (? x)))" vorkommt, liefere
;; T zur"uck, sonst NIL.
(defun occur-check-fails (var term)
  (cond 
   ;; Basisfall 1: term ist flach
   ((or (atom term) (null term)) 
    NIL)
   
   ;; Basisfall 2: term ist Variable
   ((is-var term)                
    (eq (get-varname term) var))
   
   ;; Rekursion 1: betrachte erstes Arg von term
   ((occur-check-fails var (first term)) 
    T)
   
   ;; Rekursion 2: betrachte nun die weiteren Argumente
   (T
    (occur-check-fails var (rest term)))))

;;; ============================================================================
;;; SUBSTITUTE-VAR <LISTE VON PRAEDIKATEN> <VARIABLE> <TERM>
;; Liefere die Pr"adikate zur"uck, die entstehen, wenn die Variable durch den
;; Term substituiert wird. Tats"achlich ruft sich die Funktion rekursiv auf und
;; bei diesen Aufrufen ist der Parameter 'pred' manchmal *kein* Pr"adikat, 
;; sondern eine Liste von Pr"adikaten/Termen oder ein Pr"adikat/Term. 
;; Diese schlampige Bezeichnungsweise tritt noch an anderen Stellen auf... 
;; Asche auf mein Haupt :-)
(defun substitute-var (pred var term)
  (cond 
   ;; 1. Basisfall: Flache Terme etc. -> nix zu tun
   ((or (atom pred) (null pred))
    pred)
   ;; 2. Basisfall: pred ist Variable
   ((is-var pred)
    (if (eq (get-varname pred) (get-varname var))
        ;; Namen stimmen "uberein: gib term zur"uck
        term
      ;; else: andere Variable -> nix zu tun
      pred))
   ;; Rekursiver Aufruf: Behandle erstes Element von pred und klebe das
   ;; Ergebnis an das Ergebnis aus der Bearbeitung des Restes von pred an...
   (T
    (cons (substitute-var (first pred) var term)
          (substitute-var (rest pred) var term)))))

;;; ============================================================================
;;; MGU <LISTE VON PRAEDIKATEN>
;; Liefert den most-General-Unifier der Pr"aedikate. NIL wird zur"uck-
;; geliefert, wenn alle identisch sind. :OCCUR-CHECK bzw. :NO-VAR bedeuten
;; Mi"serfolg. mgu macht nur die Pr"adikate disjunkt bzgl. ihrer 
;; Variablensymbole, die Hauptarbeit geschieht in mgu-1.
(defun mgu (plist) 
  (setf *P* (do-replace-varnames plist))
  (mgu-1 *P*))

;;; ============================================================================
;;; MGU-1 <LISTE VON PRAEDIKATEN>
;; Formulierung des Algorithmus' aus der Vorlesung:
;; In Schleife:
;;   Bestimme Unterschiede
;;   Keine Unterschiede ? -> Erfolg
;;   W"ahle Variable und Term (occur-check in find-term-in-difflist)
;;   Keine Variable ? -> mit :NO_VAR abbrechen
;;   Variable taucht in allen Termen auf ? -> mit :OCCUR-CHECK abbrechen
;;   Wende so erhaltene Substitution auf Praedikate an.
;;   wiederhole Schleife auf "neuen" Praedikaten.
;; 
(defun mgu-1 (p)
  (let ((var)   ;; zum Merken einer Variable...
        (term)) ;; ...und eines Terms aus der Unterschiedsliste 
    (do (;; SCHLEIFEN-PARAMETER diff mgu terminate
         (diff (setq *DIFF* (get-diff-list p))  ;; Unterschiedsliste bestimmen 
               (setq *DIFF* (get-diff-list p))) ;; (und *DIFF* wird gesetzt)
         (mgu nil)                           ;; mgu ist anfangs NIL = keine Subs. 
         (terminate nil)) ;; Flag f"ur Abbruch:  NIL, :OCCUR-CHECK oder :NO-VAR
        (;; SCHLEIFEN-ABBRUCHBEDINGUNGEN
         (or (not diff) terminate)    
         (if terminate terminate mgu)) ;; R"uckgabewert: Liste von Substitutionen
      ;; oder Fehlercode
      ;; SCHLEIFENBLOCK
      ;; diff ist nicht nil, terminate ist nil

      (if (setq var (find-var-in-difflist diff));; Variable in Unterschiedsliste
 
          (if (not (setq term (find-term-in-difflist var diff))) ;; aber kein 
              (setq terminate :occur-check)  ;;  Term, der den occur-check besteht
            ;; ELSE: Unifikation m"oglich
            (progn
              ;; Erweitere mgu
              (setq mgu (cons (new-substitution var term) mgu))
              ;; Wende die neue Substitution auf p und q an und aktualisiere *U*
              (setq *U* (setq p (substitute-var p var term)))))
        ;; ELSE: Keine Variable in diff -> Unifikation nicht m"oglich
        (setq terminate :no-var)))))

;;; ============================================================================
;;; SHOW-MGU <LISTE VON PRAEDIKATEN>
;; "Netter" Aufruf von MGU :-)
;; Wichtig: Dies special-Variablen werden erst als Seiteneffekt durch den 
;; Aufruf von MGU gesetzt. 
(defun show-mgu (p)
  (setq *U* NIL)
  (setq *MGU* (mgu p))
  (format T "Praedikate: ~s~%" *P*)
  (cond 
   ((eq *MGU* :OCCUR-CHECK)
    (format T "Occur-check fehlgeschlagen bei Unterschiedsliste ~s~%" *DIFF*))
   ((eq *MGU* :NO-VAR)
    (format T "Keine Variable in Unterschiedsliste ~s~%" *DIFF*))
   ((null *MGU*)
    (format T "Praedikate sind identisch. mgu = id~%"))
   (T 
    (format T "mgu ist ~s, ~%das unifizierte Praedikat ist ~s~%" 
            *MGU* 
            (first (remove-duplicates *U* :test #'equal))))))

;;; ============================================================================
;;; SHOW-ALL
;; Starte den Algorithmus f"ur alle Beispiele
(defun show-all ()
  (show-mgu *A1*)
  (terpri)
  (show-mgu *A2*)
  (terpri)
  (show-mgu *A3*)
  (terpri)
  (show-mgu *A4*)
  (terpri)
  (show-mgu *A5*)
)