logic.lisp

(defvar true t)
(defvar false nil)

(defun -> (p q) (or (not p) q))

(defun booleanp (formula)
  (or (eq formula 'true) (eq formula 'false)
      (eq formula t) (eq formula nil) ))

(defun atomic-fomula-p (formula)
  (or (booleanp formula)
      (symbolp formula) ))

(defun arity (formula)
  (when (atomic-fomula-p formula)
    (error "no arity for an atomic formula: ~s" formula) )
  (length (cdr formula)) )

(defun wffp (formula)
  (or (atomic-fomula-p formula) (predicatep formula)) )

(defun predicatep (formula)
  (or (logical-predicate-p formula)
      (math-predicate-p formula)
      (generic-predicate-p formula) ))

(defun logical-predicate-p (formula)
  (or (negationp formula)
      (conjunctionp formula)
      (disjunctionp formula)
      (implicationp formula) ))

(defun negationp (formula)
  (and (consp formula)
       (eq (car formula) 'not)
       (= (arity formula) 1)
       (wffp (cadr formula)) ))

(defun conjunctionp (formula)
  (and (consp formula)
       (eq (car formula) 'and)
       (every #'wffp (cdr formula)) ))

(defun disjunctionp (formula)
  (and (consp formula)
       (eq (car formula) 'or)
       (every #'wffp (cdr formula)) ))

(defun implicationp (formula)
  (and (consp formula)
       (eq (car formula) '->)
       (= (arity formula) 2)
       (every #'wffp (cdr formula)) ))

(defun math-predicate-p (formula)
  (and (consp formula)
       (or
         (and (= (arity formula) 1)
              (case (car formula) ((evenp oddp zerop plusp minusp) t)) )
         (and (= (arity formula) 2)
              (case (car formula) ((= /= < > <= >=) t)) ))
       (every #'math-formula-p (cdr formula)) ))

(defun math-formula-p (formula)
  (or
    (numberp formula)
    (symbolp formula)
    (and (consp formula)
         (or
           (and (>= (arity formula) 0)
                (case (car formula) ((+ * lcm gcd) t)) )
           (and (= (arity formula) 1)
                (case (car formula) ((signum abs exp) t) ))
           (and (<= 1 (arity formula) 2)
                (case (car formula) ((log expt) t)) )
           (and (>= (arity formula) 1)
                (case (car formula) ((- / max min) t)) )
           (and (= (arity formula) 2)
                (case (car formula) ((mod rem) t)) ))
         (every #'math-formula-p (cdr formula)) )))

(defun generic-predicate-p (formula)
  (and (not (logical-predicate-p formula))
       (not (math-predicate-p formula))
       (not (math-formula-p formula))
       (consp formula)
       (symbolp (car formula))
       (symbol-function (car formula)) ))

(defun normalize (wff)
  (unless (wffp wff)
    (error "cannot normalize ill-formed formula: ~s" wff) )
  (cond ((atomic-fomula-p wff) wff)
        ((negationp wff)
         (normalize-negation (cadr wff)))
        ((implicationp wff)
         (normalize-implication
           (normalize (cadr wff))
           (normalize (caddr wff)) ))
        ((conjunctionp wff) (normalize-conjunction (cdr wff)) )
        ((disjunctionp wff) (normalize-disjunction (cdr wff)) )
        ((math-predicate-p wff) wff)
        ((generic-predicate-p wff) wff) ))

(defun normalize-negation (wff)
  (cond ((atomic-fomula-p wff) (list 'not wff))
        ((negationp wff) (normalize (cadr wff)))
        ((conjunctionp wff)
         (normalize-disjunction (mapcar #'normalize-negation (cdr wff))) )
        ((disjunctionp wff)
         (normalize-conjunction (mapcar #'normalize-negation (cdr wff))) )
        ((implicationp wff)
         (list 'and (normalize (cadr wff))
               (normalize (list 'not (normalize (caddr wff)))) ))
        ((math-predicate-p wff)
         (let ((dedicated-one (case (car wff)
                                ((=) '/=) ((/=) '=)
                                ((>) '<=) ((<) '>=)
                                ((>=) '<) ((<=) '>)
                                ((evenp) 'oddp) ((oddp) 'evenp) )))
           (if dedicated-one
             (cons dedicated-one (cdr wff))
             (list 'not wff) )))
        ((generic-predicate-p wff) (list 'not wff)) ))

(defun normalize-conjunction (body)
  (cons 'and (mapcar #'normalize body)) )

(defun normalize-disjunction (body)
  (cons 'or (mapcar #'normalize body)) )

(defun normalize-implication (p q)
  (list 'or (normalize (list 'not (normalize p))) (normalize q)) )

(defun flatten (wff)
  (let ((formula (normalize wff)))
    (cond ((atomic-fomula-p formula) formula)
          ((math-predicate-p formula) formula)
          ((generic-predicate-p formula) formula)
          ((negationp formula) formula) ; (cdr fomula) must be an atomic one
          ((conjunctionp formula) (flatten-conjunction (cdr formula)))
          ((disjunctionp formula) (flatten-disjunction (cdr formula))) )))

(defun expected-wff-type-p (type wff)
  (or (and (eq type 'and) (conjunctionp wff))
      (and (eq type 'or) (disjunctionp wff)) ))

(defun invert-wff-type-p (type wff)
  (or (and (eq type 'and) (disjunctionp wff))
      (and (eq type 'or) (conjunctionp wff)) ))

(defun flatten-of (type body)
  (loop for clause in body
        when (atomic-fomula-p clause) collect clause
        when (math-predicate-p clause) collect clause
        when (generic-predicate-p clause) collect clause
        when (negationp clause) collect clause
        when (expected-wff-type-p type clause) nconc (cdr clause)
        when (invert-wff-type-p type clause) collect clause ))

(defun flatten-conjunction (body)
  (cons 'and (flatten-of 'and (mapcar #'flatten body)) ))

(defun flatten-disjunction (body)
  (cons 'or (flatten-of 'or (mapcar #'flatten body)) ))


(defun distribution-of (type wff)
  (let ((formula (normalize wff)))
    (cond ((atomic-fomula-p formula) formula)
          ((math-predicate-p formula) formula)
          ((generic-predicate-p formula) formula)
          ((negationp formula) formula)
          ((invert-wff-type-p type formula) formula)
          ((expected-wff-type-p type formula)
           (do-distribution-of type formula) ))))

(defun invert-logic-type (type)
  (ecase type
    ((and) 'or)
    ((or) 'and) ))

(defun do-binary-distribution-of (type p q)
  (flatten
    (cond ((and (invert-wff-type-p type p) (invert-wff-type-p type q))
           (cons (invert-logic-type type)
                 (loop for i in (cdr p)
                       nconc (loop for j in (cdr q) collect (list type i j)) )))
          ((invert-wff-type-p type q)
           (cons (invert-logic-type type)
                 (loop for i in (cdr q) collect (list type p i)) ))
          ((invert-wff-type-p type p)
           (cons (invert-logic-type type)
                 (loop for i in (cdr p) collect (list type i q)) ))
          (t (list type p q)) )))

(defun do-distribution-of (type formula)
  (reduce (lambda (p q) (flatten (do-binary-distribution-of type p q)))
          (cdr formula) ))

(defun reduction (wff)
  (cond ((atomic-fomula-p wff) wff)
        ((math-predicate-p wff) wff)
        ((generic-predicate-p wff) wff)
        ((negationp wff) (reduce-negation (cdr wff)))
        ((conjunctionp wff) (reduce-conjunction (cdr wff)))
        ((disjunctionp wff) (reduce-disjunction (cdr wff)))
        ((implicationp wff) (reduction (normalize wff))) ))

(defun reduce-negation (wff)
  (list 'not (reduction (car wff))) )

(defun truep (wff)
  (or (and (booleanp wff) (or (eq wff 'true) (eq wff true)))
      ;; stub
      ))

(defun falsep (wff)
  (or (and (booleanp wff) (or (eq wff 'false) (not wff)))
      ;; stub
      ))

(defun orthogonalp (lhs rhs)
  (or (and (truep lhs) (falsep rhs))
      (and (falsep lhs) (truep rhs))
      (and (math-predicate-p lhs) (math-predicate-p rhs)
           (orthogonal-math-predicate-p lhs rhs) )
      (generic-orthogonal-predicate-p lhs rhs) ))

(defun orthogonal-math-predicate-p (lhs rhs)
  (cond ((or (and (eq (car lhs) '=) (eq (car rhs) '/=))
             (and (eq (car lhs) '/=) (eq (car rhs) '=))
             (and (eq (car lhs) '<) (eq (car rhs) '>=))
             (and (eq (car lhs) '>=) (eq (car rhs) '<))
             (and (eq (car lhs) '>) (eq (car rhs) '<=))
             (and (eq (car lhs) '<=) (eq (car rhs) '>))
             (and (eq (car lhs) 'evenp) (eq (car rhs) 'oddp))
             (and (eq (car lhs) 'oddp) (eq (car rhs) 'evenp)) )
         (equal (cdr lhs) (cdr rhs)) )))

(defun generic-orthogonal-predicate-p (lhs rhs)
  (or (and (negationp lhs) (not (negationp rhs))
           (equal (cadr lhs) rhs) )
      (and (not (negationp lhs)) (negationp rhs)
           (equal lhs (cadr rhs)) )))

(defun reduce-conjunction (body)
  (cond ((= (length body) 0)
         'true ) ; (and)
        ((= (length body) 1)
         (reduction (car body)) )
        ((= (length body) 2)
         (if (orthogonalp (first body) (second body))
           'false
           (let ((lhs (reduction (first body)))
                 (rhs (reduction (second body))) )
             (cond ((and (booleanp lhs) (booleanp rhs))
                    (if (and (truep lhs) (truep rhs)) 'true 'false) )
                   ((booleanp lhs)
                    (if (truep lhs) rhs 'false) )
                   ((booleanp rhs)
                    (if (truep rhs) lhs 'false) )
                   (t (list 'and lhs rhs)) ))))
        (t (let ((reduced
                   (loop for f in body
                         for rf = (reduction f)
                         when (and (booleanp rf) (falsep rf))
                           return (list 'false)
                         when (not (truep rf))
                           collect rf )))
             (if (<= (length reduced) 2)
               (reduce-conjunction reduced)
               (cons 'and reduced) )))))

(defun reduce-disjunction (body)
  (cond ((= (length body) 0)
         'false )  ; (or)
        ((= (length body) 1)
         (reduction (car body)) )
        ((= (length body) 2)
         (if (orthogonalp (first body) (second body))
           'true
           (let ((lhs (reduction (first body)))
                 (rhs (reduction (second body))) )
             (cond ((and (booleanp lhs) (booleanp rhs))
                    (if (not (and (falsep lhs) (falsep rhs))) 'true 'false) )
                   ((booleanp lhs)
                    (if (truep lhs) rhs 'true) )
                   ((booleanp rhs)
                    (if (truep rhs) lhs 'true) )
                   (t (list 'or lhs rhs)) ))))
        (t (let ((reduced
                   (loop for f in body
                         for rf = (reduction f)
                         when (and (booleanp rf) (truep rf))
                           return (list 'true)
                         when (not (falsep rf))
                           collect rf )))
             (if (<= (length reduced) 2)
               (reduce-disjunction reduced)
               (cons 'or reduced) )))))

;; distribution of disjunction over conjunction makes a CNF
;; (or P (and Q R)) <=> (and (or P Q) (or P R))
;; (or P (and Q R) (and S T))
;;   <=> (or P (or (and Q R) (and S T)))
;;   <=> (or P (and (or (and Q R) S)
;;                  (or (and Q R) T) ))
;;   <=> (or P (and (and (or Q S) (or R S))
;;                  (and (or Q T) (or R T)) ))
;;   <=> (and (or P (and (or Q S) (or R S)))
;;            (or P (and (or Q T) (or R T))) )
;;   <=> (and (and (or P (or Q S)) (or P (or R S)))
;;            (and (or P (or Q T)) (or P (or R T)))
;;   <=> (and (and (or P Q S) (or P R S))
;;            (and (or P Q T) (or P R T)))
;;   <=> (and (or P Q S) (or P R S) (or P Q T) (or P R T))
(defun normalize-conjunction-form (wff)
  (reduction (flatten (distribution-of 'or (normalize wff)))) )

;; distribution of conjunction over disjunction makes a DNF
;; (and P (or Q R)) <=> (or (P and Q) (P and R))
;; (and P (or Q R) (or S T))
;;   <=> (and P (and (or Q R) (or S T)))
;;   <=> (and P (or (and (or Q R) S) (and (or Q R) T)))
;;   <=> (or (and P (or Q R) S)
;;           (and P (or Q R) T))
;;   <=> (or (and (and P (or Q R)) S)
;;           (and (and P (or Q R)) T))
;;   <=> (or (and (or (and P Q) (and P R)) S)
;;           (and (or (and P Q) (and P R)) T))
;;   <=> (or (or (and (and P Q) S) (and (and P R) S))
;;           (or (and (and P Q) T) (and (and P R) T)))
;;   <=> (or (or (and P Q S) (and P R S))
;;           (or (and P Q T) (and P R T)))
;;   <=> (or (and P Q S) (and P R S) (and P Q T) (and P R T))
(defun normalize-disjunction-form (wff)
  (reduction (flatten (distribution-of 'and (normalize wff)))) )

;;
(defmacro lambda-abstraction (fn args wff)
  `(defun ,fn ,args ,(eval wff)) )

(reduction '(not (p x))) が nil になるバグを修正