hivecast-sdk/packages/oracle/core/help/trs.help.md

symbol, signature, package

symbol	signature	package
trs	(trs ...)	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

;; 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

(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

;; 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

;; 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

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

See Also

• oracle - Oracle integration and semantic operations