;; -*- Mode: Lisp; -*-

;;;; Algebra system for CPS
;;;; File name: algebra.lsp
;;;;  modified: Thursday, January 10, 2008 at 10:30:18 by Ken Forbus

;;; Copyright (c) 1986-1993
;;;   Kenneth D. Forbus and Johan de Kleer
;;;   All Rights Reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

#|
A problem consists of an equation in the unknown, X.  The goal is
to construct an equation that has just X on the left hand side,
and no occurences of X on the RHS.

A state in these problems has the form (= <lhs> <rhs>).  The
sides are just s-expressions corresponding to mathematical terms.
We provide a basic simplification program in another file to take
care of mundane stuff like collapsing constants.

This file contains the operator descriptions and CPS hooks.  The
function SETUP-ALGEBRA-PROBLEM sets up the algebra problem space.

This version uses the CLOS-based version of CPS
|#


(defclass algebra-problem (problem)
  ((unknown :reader unknown :initarg :unknown
            :documentation "The unknown being solved for")))


;;; Expression accessors and predicates
;;; ----------------------------------------------------------------------------
(defmacro lhs (x) 
  "The left-hand side of equation."
  `(cadr ,x))
  
(defmacro rhs (x) 
  "The right-hand side of equation."
  `(caddr ,x))

(defun occurs-in? (exp1 exp2) 
  "True if expression 1 is contained somewhere in expression 2."
  (cond ((equal exp1 exp2) t)
        ((null exp2) nil)
        ((listp exp2)
         (or (occurs-in? exp1 (car exp2))
             (occurs-in? exp1 (cdr exp2))))))

(defun has-unknown? (exp problem)
  "True if expression contains unknown value."
   (occurs-in? (unknown problem) exp))
   
(defun no-unknown? (exp problem) 
  "True if expression contains no unknown values."
  (not (occurs-in? (unknown problem) exp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Problem space interface procedures
;;; ----------------------------------------------------------------------------
(defmethod goal-found? ((state list) (problem algebra-problem))
   "Has goal of algebra problem been met?"
   (and (eq (lhs state) (unknown problem)) ;; LHS = X
        (no-unknown? (rhs state) problem))) ;; No X's in RHS.

(defmethod apply-operator ((operator list) (state list) (problem algebra-problem))
  "Given an algebra operator and a state, apply the operator to the state."
  ;; Operators take the form (<name> <procedure>)
  (funcall (cadr operator) state problem))

(defmethod states-identical? ((state1 list) (state2 list)
                              (problem algebra-problem))
  ;; This is undecidable in general, so we only worry about the simple case here.
  (equal state1 state2))

(defmethod solution-element->string ((state list) (op-instance list)
                                     (problem algebra-problem))
  "Return single step in solved plan (or derivation) as string."
  (format nil "~A, via ~A" (state->string state problem)
    (car op-instance)))

(defmethod state->string ((state list) (problem algebra-problem))
  (format nil "~A" state))

(defmethod distance-remaining ((state list) (problem algebra-problem))
  (algebra-distance state (unknown problem)))

;;;; Computing distance estimates for algebra problems
;; A reasonable heuristic is the sum of the depths of
;; occurrences of X in the expression tree.

(defun algebra-distance (expr the-unknown)
  "Estimate how close this expression is to solution, return number."
  (labels ((sum-tree-depth
	    (exp depth)
	    (cond ((null exp) 0)
		  ((eq exp the-unknown) depth)
		  ((not (listp exp)) 0)
		  (t (+ (sum-tree-depth (car exp) (1+ depth))
			(sum-tree-depth (cdr exp) depth))))))
    (+ (sum-tree-depth (lhs expr) 1)
       (sum-tree-depth (rhs expr) 1))))

(defun setup-algebra-problem (the-unknown)
  "Create an generic algebra 'problem space'."
  (make-instance 'algebra-problem
   :name the-unknown
   :unknown the-unknown
   :operators '((isolate-log try-isolate-log)
                (isolate-sum try-isolate-sum)
                (isolate-difference try-isolate-difference)
                (isolate-square try-isolate-square)
                (collect-product-difference try-collect-prod-diff)
                (attract-log-sum try-attract-log-sum)
                (canonicalize try-canonicalization))))

;; A test case
(defvar *bundy* '(= (+ (log (+ x 1) E) (log (- x 1) E)) C)
  "A single example problem from Alan Bundy's reasoner.")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; Isolation techniques

(defun try-isolate-log (form problem &aux bindings)
  (setq bindings
        (match `(= (log (? arg ,(lambda (e) (has-unknown? e problem)))
                  (? base ,(lambda (e) (no-unknown? e problem))))
		   (? rhs ,(lambda (e) (no-unknown? e problem))))
	       form))
  (unless (eq bindings :fail)
    `(,(cons `(isolate-log-instances ,form)
	     (simplify
	      (substitute-in `(= (? arg) (expt (? base) (? rhs)))
			     bindings))))))

(defun try-isolate-square (form problem &aux bindings)
  (setq bindings
	(match `(= (sqr (? arg ,(lambda (e) (has-unknown? e problem))))
		   (? rhs ,(lambda (e) (no-unknown? e problem))))
	       form))
  (unless (eq bindings :fail)
    `(,(cons `(isolate-square ,form)
	     (simplify (substitute-in `(= (? arg) (sqrt (? rhs)))
				      bindings))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun try-isolate-sum (form problem &aux bindings)
  (setq bindings
	(match `(= (+ (?? pre ,(lambda (e) (no-unknown? e problem)))
		      (? arg ,(lambda (e) (has-unknown? e problem)))
		      (?? post ,(lambda (e) (no-unknown? e problem))))
		   (? rhs ,(lambda (e) (no-unknown? e problem))))
	       form))
  (unless (eq bindings :fail)
    `(,(cons `(isolate-sum ,form)
	     (simplify
	      (substitute-in `(= (? arg)
				 (- (? rhs) (+ (?? pre) (?? post))))
			     bindings))))))

(defun try-isolate-difference (form problem &aux bindings)
  (setq bindings
	(match `(= (- (? arg1 ,(lambda (e) (has-unknown? e problem)))
		      (? arg2 ,(lambda (e) (no-unknown? e problem))))
		   (? rhs ,(lambda (e) (no-unknown? e problem))))
	       form))
  (unless (eq bindings :fail)
    `(,(cons `(isolate-difference ,form)
	     (simplify (substitute-in `(= (? arg1) (+ (? rhs) (? arg2)))
				      bindings))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Collection Methods

;;; Sum collection:
;;; Given (U+V)*(U-V), turn it into U^2-V^2 
;;; Use only on "least dominating terms" in X.
;;; U must have an occurrence of X.

(defun find-least-dominating-terms (exp problem &aux result xts)
  "Return a list of the least dominating terms in the given expression."
  (cond ((or (null exp) (not (listp exp))) nil)
        (t (setq xts (remove-if (lambda (e) (no-unknown? e problem)) exp))
           (cond ((cdr xts) (setq result (list exp))
                  (dolist (xt xts result)
                    (setq result
                          (nconc result
                                (find-least-dominating-terms xt problem)))))
                 (t 
                  (setq result
                        (nconc result
                               (find-least-dominating-terms (car xts) problem))))))))

(defun try-collect-prod-diff (form problem &aux bindings results)
 (dolist (ldt (find-least-dominating-terms form problem) results)
  (setq bindings
	(match `(* (+ (? v ,(lambda (e) (no-unknown? e problem)))
		      (? u ,(lambda (e) (has-unknown? e problem))))
		   (- (? u) (? v)))
	       ldt))
  (unless (eq bindings :fail)
   (push (cons `(collect-product-sum ,ldt)
	       (simplify
		(subst (substitute-in
			`(- (sqr (? u)) (sqr (? v)))
			bindings)
		       ldt form)))
	 results))))

;;; Attraction rule for logs
;;; (log U W) + (log V W) => (log (* U V) W)
;;; where U, V contain X and W doesn't.

(defun try-attract-log-sum (form problem &aux results bindings)
 (dolist (ldt (find-least-dominating-terms form problem)
	      results)
  (setq bindings
	(match `(+ (log (? u ,(lambda (e) (has-unknown? e problem)))
			(? w ,(lambda (e) (no-unknown? e problem))))
		   (log (? v ,(lambda (e) (has-unknown? e problem)))
			(? w)))
	       ldt))
  (unless (eq bindings :fail)
   (push (cons `(Attract-log-sum ,ldt)
	       (simplify
		(subst (substitute-in
			`(log (* (? u) (? v)) (? w))
			bindings)
		       ldt form)))
	 results))))

(defun try-canonicalization (form problem &aux result)
  (declare (ignore problem))
  (setq result (simplify form))
  (unless (equal result form)
    `(,(cons `(Canonicalization ,form)
	     result))))