term-rewrite-system/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))

(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))))