---
symbol: trs
signature: "(trs ...)"
package: oracle/core
---

# trs - Term Rewriting System

Pattern-based transformation of symbolic expressions.

## When to Use

- Simplify algebraic expressions
- Transform code ASTs
- Implement domain-specific optimizations
- Normalize data structures

## Primitives

| Primitive | Signature | Description |
|-----------|-----------|-------------|
| `make-rule` | `(make-rule pattern template)` | Create rewrite rule |
| `make-rule-where` | `(make-rule-where pattern template guard)` | Rule with condition |
| `rule?` | `(rule? x)` | Is rewrite rule? |
| `rewrite-once` | `(rewrite-once rules term)` | Apply first matching rule |
| `rewrite-fixpoint` | `(rewrite-fixpoint rules term)` | Rewrite until no change |
| `rewrite-trace` | `(rewrite-trace rules term)` | Rewrite with trace |
| `rewrite-conflicts` | `(rewrite-conflicts rules term)` | Find conflicting rules |
| `match-pattern` | `(match-pattern pattern term)` | Match and extract bindings |
| `substitute-template` | `(substitute-template template bindings)` | Apply bindings |

## Pattern Syntax

- `?x` - Variable, matches anything
- `??xs` - Splicing variable, matches zero or more
- Literal symbols and lists match exactly

## Quick Start

```lisp
;; Simple rule: (+ 0 x) => x
(define rule-add-zero
  (make-rule '(+ 0 ?x) '?x))

;; Apply once
(rewrite-once (list rule-add-zero) '(+ 0 5))
; => 5

;; Multiple rules
(define arith-rules
  (list
    (make-rule '(+ 0 ?x) '?x)
    (make-rule '(+ ?x 0) '?x)
    (make-rule '(* 1 ?x) '?x)
    (make-rule '(* ?x 1) '?x)
    (make-rule '(* 0 ?x) '0)
    (make-rule '(- ?x ?x) '0)))

;; Rewrite to fixpoint
(rewrite-fixpoint arith-rules '(+ (* 1 (- y y)) x))
; => x
```

## Common Patterns

### Algebraic Simplification
```lisp
(define simplify-rules
  (list
    ;; Identity
    (make-rule '(+ 0 ?x) '?x)
    (make-rule '(* 1 ?x) '?x)

    ;; Annihilation
    (make-rule '(* 0 ?x) '0)

    ;; Combination
    (make-rule '(+ ?x ?x) '(* 2 ?x))

    ;; Distribution
    (make-rule '(* ?a (+ ?b ?c))
               '(+ (* ?a ?b) (* ?a ?c)))))

(rewrite-fixpoint simplify-rules '(* 2 (+ x x)))
; => (+ (* 2 x) (* 2 x)) or simplified further
```

### Conditional Rules
```lisp
;; Only reduce if both numbers
(define const-fold
  (make-rule-where
    '(+ ?a ?b)
    '?result
    (lambda (bindings)
      (let ((a (cdr (assoc '?a bindings)))
            (b (cdr (assoc '?b bindings))))
        (and (number? a) (number? b)
             (list (cons '?result (+ a b))))))))

(rewrite-once (list const-fold) '(+ 2 3))  ; => 5
(rewrite-once (list const-fold) '(+ x 3))  ; => (+ x 3)
```

### Code Transformation
```lisp
;; Desugar let to lambda
(define desugar-let
  (make-rule
    '(let ((?var ?val)) ?body)
    '((lambda (?var) ?body) ?val)))

(rewrite-once (list desugar-let)
  '(let ((x 5)) (+ x 1)))
; => ((lambda (x) (+ x 1)) 5)
```

### Tracing Rewrites
```lisp
(define trace (rewrite-trace arith-rules '(+ 0 (* 1 x))))
; Returns list of intermediate forms:
; ((+ 0 (* 1 x))
;  (* 1 x)
;  x)
```

## See Also

- [oracle](oracle.help.md) - Oracle integration and semantic operations