;;; Syllogistic reasoning

;;; Copyright 1993 by Jeff Dalton

;;; A syllogism involves two premises and three sets, conventionally
;;; called A, B, and C.  The first premise relates A and B, the second
;;; relates B and C.

;;; Our basic strategy is:
;;;   1. Generate all possible worlds.
;;;   2. Filter out non-Aristotelian worlds.
;;;   3. Filter out the worlds that fail to satisfy both premises
;;;   4. Find the conclusions that are true in all remaining worlds.

;;; Terminology:
;;;   A world is a list of individuals.
;;;   An individual is a list of properties.
;;;   A property is a set name.

;;; Note that we don't actually deal with all possible worlds.  We do
;;; not bother with properties that are not mentioned in the premises,
;;; nor with duplicate individuals.  So in effect we're dealing with
;;; equivalence classes of possible worlds, with each class represented
;;; by its simplest member.

;;; In an "Aristotelian world", none of the interesting sets are empty.
;;; This is how we take into account Aristotle's view that "All A are B"
;;; is true only when there are some A (ie, that it can't be vacuously
;;; true).

;;; Premise syntax:
;;;    set ::= name | (NOT set) | (NON set)
;;;   prop ::= (ALL set [are] set)
;;;         |  (SOME set [are] set)
;;;         |  (NO set [are] set)

;;; (Syl premise1 premise2) returns a list if valid conclusions.

;;; (Equivalents premise) returns a list of equivalent premises
;;; in standard form.  It is not used when solving syllogisms, but
;;; let's you see what the standard form (if any) of a premise is.

;;; (Enumerate-syllogisms) returns a list of all valid syllogisms.

;;; (Print-syllogisms) prints all valid syllogisms in a neat form.

;;; NB To handle the nonstandard premises, we have to include the
;;; individual with no properties and filter out worlds that do
;;; not contain non-As, non-Bs, and non-Cs (as well as those that
;;; do not contain As, Bs, and Cs).

(defparameter *premise-forms*
  ;; The last two are nonstandard.
  '((all A are B)
    (all B are A)
    (some A are B)
    (no A are B)
    (some A are (not B))
    (some B are (not A))
    (some (not A) are (not B))		;not exhaustive partition
    (all (not A) are B)))		;exhaustive partition

(defun premises-in (set1 set2)
  (mapcar #'(lambda (form)
	      (sublis `((A . ,set1) (B . ,set2)) form))
	  *premise-forms*))

(defun syl (premise1 premise2)
  (let* ((a-and-b   (require-len 2 (names premise1)))
	 (b-and-c   (require-len 2 (names premise2)))
	 (b         (require-len 1 (intersection a-and-b b-and-c)))
	 (a         (require-len 1 (set-difference a-and-b b)))
	 (c         (require-len 1 (set-difference b-and-c b)))
	 (a-b-and-c (require-len 3 (union a-and-b b-and-c)))
	 (worlds    (generate-worlds a-b-and-c)))
    (find-conclusions
      (first a)
      (first c)
      (remove-if-not (conjoin (compile-filter premise1)
			      (compile-filter premise2))
		     worlds))))

(defun find-conclusions (a c worlds)
  (let ((candidates (premises-in a c)))
    (remove-if-not
      #'(lambda (candidate)
	  (every (compile-filter candidate) worlds))
      candidates)))

(defun require-len (len val)
  (if (= (length val) len)
      val
    (error "Expected ~S elements in ~S" len val)))

(defun generate-worlds (sets)
  (let* ((properties sets)
	 (individuals (powerset properties))
	 (worlds (powerset individuals)))
    ;; Now filter out worlds in which any of the sets are empty
    (let ((filters
	   (mapcan #'(lambda (set)
		       (let ((filter (compile-filter set)))
			 (list (exists filter)
			       (exists (negate filter)))))
		   sets)))
      (remove-if-not
         (reduce #'conjoin filters)
	 worlds))))

(defun powerset (set)
  (if (null set)
      (list '())
    (let ((e1 (car set))
	  (p (powerset (cdr set))))
      ;; Append subsets with e1 to subsets without e1
      (append (mapcar #'(lambda (subset) (cons e1 subset))
		      p)
	      p))))

(defun equivalents (premise)
  (let* ((a-and-b (require-len 2 (names premise)))
	 (worlds (generate-worlds a-and-b))
	 (a (first a-and-b))
	 (b (second a-and-b)))
    (let ((p-filter (compile-filter premise))
	  (candidates (premises-in a b)))
      (remove-if-not
        #'(lambda (candidate)
	    (let ((c-filter (compile-filter candidate)))
	      (every #'(lambda (world)
			 ;; If either p- or c-filter is true, both must be
			 (if (funcall p-filter world)
			     (funcall c-filter world)
			   (not (funcall c-filter world))))
		     worlds)))
	candidates))))

(defun enumerate-syllogisms ()
  (mapcan #'(lambda (premise1)
	      (mapcar #'(lambda (premise2)
			  (list premise1
				premise2
				(syl premise1 premise2)))
		      (premises-in 'b 'c)))
	  (premises-in 'a 'b)))

(defun print-syllogisms (&optional (out t))
  (dolist (s (enumerate-syllogisms))
    (let ((p1 (flatten (first s)))
	  (p2 (flatten (second s)))
	  (c* (mapcar #'flatten (third s))))
      (format out "~&~{~S~^ ~}, ~{~S~^ ~} -> ~A"
	      p1
	      p2
	      (if (null c*)
		  "No conclusion"
		(format nil "~{~{~S~^ ~}~^, ~}" c*)))))
  (format out "~%"))

(defun flatten (tree)
  (labels ((flat (at result)
	     (cond ((null at) result)
		   ((atom at) (cons at result))
		   (t (flat (cdr at) (flat (car at) result))))))
    (nreverse (flat tree '()))))

;;; Filter compiler

(defun set1 (p)
  (second p))

(defun set2 (p)
  (if (eq (third p) 'are) (fourth p) (third p)))

(defun names (p) ; -> list of names
  (cond ((symbolp p) (list p))
	((atom p) (error "What is this ~S?" p))
	(t (ecase (first p)
	     ((not non)
	      (names (second p)))
	     ((all some no)
	      (union (names (set1 p)) (names (set2 p))))))))

(defun compile-filter (p) ; -> predicate: world -> t/f
  (cond ((symbolp p)
	 (partial-apply #'member p))
	((atom p)
	 (error "Invalid filter: ~S." p))
	((member (first p) '(not non))
	 (negate (compile-filter (second p))))
	(t
	 (let ((p1 (compile-filter (set1 p)))
	       (p2 (compile-filter (set2 p))))
	   (ecase (first p)
	     ((all)
	      (all (disjoin (negate p1) p2))) 	;p1 implies p2
	     ((some)
	      (exists (conjoin p1 p2)))		;p1 and p2
	     ((no)
	      (all				;p1 implies not p2
	       (disjoin (negate p1) (negate p2)))))))))

(defun partial-apply (f x)
  #'(lambda (y) (funcall f x y)))

(defun negate (pred)
  #'(lambda (x) (not (funcall pred x))))

(defun all (pred)
  (partial-apply #'every pred))

(defun exists (pred)
  (partial-apply #'some pred))

(defun disjoin (p1 p2)
  #'(lambda (x) (or (funcall p1 x) (funcall p2 x))))

(defun conjoin (p1 p2)
  #'(lambda (x) (and (funcall p1 x) (funcall p2 x))))

;;; Memoization

(defvar *all-memoized-functions* '())

(defun memoize (name &key (test #'equal))
  (unless (get name 'memo-table)
    (let ((table (make-hash-table :test test)))
      (setf (get name 'memo-table) table)
      (shiftf (get name 'original-def)
	      (symbol-function name)
	      (make-memoized-function (symbol-function name) table))
      (push name *all-memoized-functions*)
      name)))

(defun make-memoized-function (fn table)
  #'(lambda (&rest args)
      (multiple-value-bind (value found-p)
	  (gethash args table)
	(if found-p
	    value
	    (setf (gethash args table) (apply fn args))))))

(defun clear-all-memos ()
  (mapc #'clear-memo *all-memoized-functions*))

(defun clear-memo (name)
  (when (get name 'memo-table)
    (clrhash (get name 'memo-table))))

(memoize 'generate-worlds)

;;; End