scheme-test-programs/logic/t-term-rewriting.scm

;; import lists/standard.scm logic/term-rewrite.scm

(define (test name sys in out)
  (print `(applying ,name to ,in))
  (let ((res (sys in)))
    (if (equal? res out)
	(print `(success ==> ,out))
	(print `(failed with ,res !)))))

(define trs-logic-1
  (compile-system
   '(((<-> x y) (and (-> x y) (-> y x)))
     ((-> x y) (or (not x) y)))))

(test 'trs-logic-1 trs-logic-1 'foo
      'foo)
(test 'trs-logic-1 trs-logic-1 '(foo bar)
      '(foo bar))
(test 'trs-logic-1 trs-logic-1 '(<-> p q)
      '(and (or (not p) q) (or (not q) p)))
(newline)

(define trs-arith-1
  (compile-system
   '(((+ x 0) x)
     ((+ 0 x) x)
     ((* x 1) x)
     ((* 1 x) x)
     ((+ (- x) x) 0)
     ((+ x (- x)) 0))))

(test 'trs-arith-1 trs-arith-1 '(+ 7 (* 1 0))
      '7)
(test 'trs-arith-1 trs-arith-1 '(* (+ 0 1) 5)
      '5)
(newline)

(define trs-logic-2
  (compile-system
   '(((and x (not x)) #f)
     ((and (not x) x) #f)
     ((or x (not x)) #t)
     ((or (not x) x) #t)

     ((and #t #t) #t)
     ((or #t x) #t)
     ((or x #t) #t)

     ((and #f x) #f)
     ((and x #f) #f)
     ((or #f #f) #f))))

(define trs-cnf
  (compile-system
   '(((not (not x)) x)

     ((not (and x y)) (or (not x) (not y)))
     ((not (or x y)) (and (not x) (not y)))

     ((or x (and y z)) (and (or x y) (or x z)))
     ((or (and x y) z) (and (or x z) (or y z))))))

(define trs-arith-2
  ;; this really illustrates limitations of TRS
  ;;
  ;; hacked together to try to repeat the example
  ;; (a + b)^2 = a^2 + 2ab + b^2
  ;; from
  ;;
  ;; <http://www.meta-environment.org/doc/books/extraction-transformation/term-rewriting/term-rewriting.html>
  (compile-system
   '(((^ x 2) (* x x))
     ((* k (+ a b)) (+ (* k a) (* k b)))
     ((* (+ a b) k) (+ (* a k) (* b k)))
     ((+ (* a b) (+ (* b a) z)) (+ (* 2 a b) z))
     ((+ (+ u v) w) (+ u (+ v w))))))

(test 'trs-arith-2 trs-arith-2
      '(^ (+ a b) 2)
      '(+ (* a a) (+ (* 2 b a) (* b b))))
(newline)

(define trs-peano
  (compile-system
   '(((+ (z) x) x)
     ((+ (s x) y) (s (+ x y)))

     ((* (z) x) (z))
     ((* (s x) y) (+ (* x y) y)))))

(define (number->peano n)
  (if (= n 0)
      '(z)
      `(s ,(number->peano (- n 1)))))

(test 'trs-peano trs-peano `(+ ,(number->peano 10)
			       ,(number->peano 4))
      (number->peano 14))
(test 'trs-peano trs-peano `(* ,(number->peano 8)
			       ,(number->peano 7))
      (number->peano 56))
;; (test 'trs-peano trs-peano `(* ,(number->peano 10)
;; 			       ,(number->peano 7))
;;       (number->peano 70))
;; (test 'trs-peano trs-peano `(* ,(number->peano 8)
;; 			       ,(number->peano 10))
;;       (number->peano 80))
;; (test 'trs-peano trs-peano `(* ,(number->peano 12)
;; 			       ,(number->peano 10))
;;       (number->peano 120))
;; (test 'trs-peano trs-peano `(* ,(number->peano 11)
;; 			       ,(number->peano 13))
;;       (number->peano 143))
;; (test 'trs-peano trs-peano `(* ,(number->peano 21)
;; 			       ,(number->peano 23))
;;       (number->peano 483))
;; (test 'trs-peano trs-peano `(* ,(number->peano 28)
;; 			       ,(number->peano 27))
;;       (number->peano 756))
(newline)

(define trs-klop
  ;; taken from
  ;;
  ;; http://www.informatik.uni-bremen.de/agbkb/lehre/rbs/texte/Klop-TR.pdf
  ;; page 17
  (compile-system
   '((($ ($ ($ (s) x) y) z)
      ($ ($ x z) ($ y z)))
     (($ ($ (k) x) y)
      x)
     (($ (i) x)
      x)
     (($ ($ ($ (b) x) y) z)
      ($ x ($ y z)))
     (($ ($ ($ (b) x) y) z)
      ($ x ($ y z))))))

(define c
  '($ ($ (s)
         ($ ($ (b) (b)) (s)))
      ($ (k) (k))))

(test 'trs-klop trs-klop `($ ($ ($ ,c x) y) z)
      '($ ($ x z) y))
(newline)

(define trs-free-group
  ;; An example of a Knuth-Bendix completion
  ;;
  ;; https://en.wikipedia.org/wiki/Word_problem_%28mathematics%29
  (compile-system
   '(((* (e) x) x)
     ((* (/ x) x) (e))
     ((* (* x y) z) (* x (* y z)))
     ((* (/ x) (* x y)) y)
     ((/ (e)) (e))
     ((* x (e)) x)
     ((/ (/ x)) x)
     ((* x (/ x)) (e))
     ((* x (* (/ x) y)) y)
     ((/ (* x y)) (* (/ y) (/ x))))))

(test 'trs-free-group trs-free-group `(* (* (/ a) a) (* b (/ b)))
      '(e))
(test 'trs-free-group trs-free-group
      ;; verify the axiom from
      ;; G. Higman and B. H. Neumann. Groups as groupoids with one law [1952]
      (let ((/ (lambda (a b) `(* ,a (/ ,b)))))
	(/ 'x (/ (/ (/ (/ 'x 'x) 'y) 'z) (/ (/ (/ 'x 'x) 'x) 'z))))
      'y)
(newline)