term-rewrite-system/chez-trs/examples.scm

;(define-module (trs examples)
;  #:use-module (trs trs)
;  #:export (logic-1
;            arith-1
;            logic-2
;            cnf
;            arith-2
;            peano
;            klop
;            free-group))

(library (examples)
(export logic-1 arith-1 logic-2 cnf arith-2 peano klop free-group)
(import (chezscheme) (trs))

(define-trs logic-1
  (==> (<-> x y) (and (-> x y) (-> y x)))
  (==> (-> x y) (or (not x) y)))

(define-trs arith-1
  (==> (+ x 0) x)
  (==> (+ 0 x) x)
  (==> (* x 1) x)
  (==> (* 1 x) x)
  (==> (+ (- x) x) 0)
  (==> (+ x (- x)) 0))

(define-trs logic-2
  (==> (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
  (==> (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>
  (==> (^ 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))))

(define-trs peano
  (==> (+ (z) x) x)
  (==> (+ (s x) y) (s (+ x y)))

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

(define-trs klop
  ;; taken from
  ;;
  ;; http://www.informatik.uni-bremen.de/agbkb/lehre/rbs/texte/Klop-TR.pdf
  ;; page 17
  (==> ($ ($ ($ (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-trs free-group
  ;; An example of a Knuth-Bendix completion
  ;;
  ;; https://en.wikipedia.org/wiki/Word_problem_%28mathematics%29
  (==> (* (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))))

)