130 lines
3.0 KiB
Markdown
130 lines
3.0 KiB
Markdown
|
---
|
||
|
|
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
|