You are looking at historical revision 23619 of this page. It may differ significantly from its current revision.

## tree-rewrite

A tree rewriting system.

## Documentation

The `tree-rewrite` library is an implementation of a structured term rewriting system based on explicit marking of redexes and an applicative order of applying them.

Function names are denoted by Scheme symbols. Variable names are symbols distringuished by a leading `$` sign. Constants can be symbols, strings and numbers. A single underscore is the anonymous variable.

Furthermore, function symbols are divided in two subsets, V- and M-function symbols. Terms over V-function symbols, constants, and variables are called V-terms.

A simple M-term is an application of an M-function symbol to V-terms; a term with M symbols is an M-term. V- and M- functional terms are represented as S-expressions of the form:

(symbol term ...)

or

(M symbol term ...)

The term grammar is the following:

<V-term> ::= number | string | symbol | var | (symbol <V-term>*) var ::= a symbol beginning with $ or simply an _ <M-term-simple> ::= (M symbol <V-term>*) <M-term> ::= (M symbol (<V-term>|<M-term>)* ) | (symbol <V-term>* <M-term> (<V-term>|<M-term>)* )

Only M-terms are subject to re-writing rules:

<re-writing-rule> ::= <pattern> => <consequent> <pattern> ::= <M-term-simple> <consequent> ::= <M-term> | <V-term>

When a subject M-term is matched against a rule, variables in the pattern are bound to the corresponding pieces in the matching term. If the matching succeeds, the `<consequent>` replaces the subject M-term with the variables substituted by the results of matching of the `<pattern>`. The resulting term should have no variables. It's an error if the subject M-term didn't match any rule.

### Procedures

*[procedure]*

`(reduce M-TERM RULES)`

The principal reduction procedure. `RULES` is a list of rewriting rules that follow the grammar above. Returns the term after all matching rules have been applied.

*[procedure]*

`(rewrite-map-tree TREE RULES)`

Applies the given set of rewrite rules to all elements in the list `TREE`. If none of the rules match a particular element, and that element is a list, recursively invokes itself on all elements in the tail of that list, and the head of the list is left in place.

*[procedure]*

`(rewrite-fold-tree RULES F INIT )`

Returns a procedure that takes in a list, and applies the given set of rewrite rules to the elements of the list. If a rule pattern matches, the values of `INIT` is replaced by the result of `(F T INIT)` where `T` is the rewritten term. If no rule matches a given element, and the element is a list, recursively invokes itself on all elements in the tail of that list, and the head of the list is left in place.

*[procedure]*

`(rewrite-fold-tree-partial RULES F INIT )`

Returns a procedure that takes in a list, and applies the given set of rewrite rules to the elements of the list. If a rule pattern matches, the values of `INIT` is replaced by the result of `(F T INIT)` where `T` is the rewritten term. If no rule matches a given element, and the element is a list, recursively invokes itself on all elements in the tail of that list, and the head of the list is discarded.

*[procedure]*

`(match-tree TREE1 TREE2 ENV)`

A non-linear match of two ordered trees, one of which may contain variables.

`TREE1` may contain variables (symbols with leading `$` sign). `TREE1` may contain several occurrences of the same variable. All these occurrences must match the same value. A variable match is entered into the environment. A variable `_` is an exception: its match is never entered into the environment. The function returns the resulting environment or `#f` if the match fails.

*[procedure]*

`(unify-trees TREE1 TREE2 ENV)`

A match/unification of two ordered trees, both of which may contain variables. The unifier is capable of finding cyclic substitutions. The trees may contain several occurrences of the same variable. All these occurrences must match the same value. A variable match is entered into the environment. A variable `_` is an exception: its match is never entered into the environment. `unify-trees` returns the resulting environment or `#f` if the unification fails.

*[procedure]*

`(substitute-vars TERM ENV)`

Finds all the vars in term and substitutes them with values given in the environment. It's an error if a term contains an unbound variable.

*[procedure]*

`(substitute-vars-open TERM ENV)`

Finds all the vars in term and substitutes them with values given in the environment. Leaves free variables as they are.

## Examples

; Arithmetics on numerals ; Transform the natural number n to the "term numeral" ; (succ ... (zero)) (define (make-numeral n) (assert (not (negative? n))) (if (zero? n) '(zero) (list 'succ (make-numeral (- n 1))))) ; Transform the term numeral back to the natural number. ; The inverse of the make-numeral above (define (eval-numeral num) (cond ((equal? num '(zero)) 0) ((and (pair? num) (eq? 'succ (car num))) (+ 1 (eval-numeral (cadr num)))) (else (error 'eval-numeral "wrong numeral " num)))) (define rule-arith '( ( (M mul (zero) $x) => (zero) ) ( (M mul $x (zero)) => (zero) ) ( (M mul (succ $x) $y) => (M add $y (M mult $x $y)) ) ( (M add (zero) $x) => $x ) ( (M add $x (zero)) => $x ) ( (M add (succ $x) $y) => (succ (M add $x $y))) ( (M add (zero) $x) => $x ) ( (M add $x (zero)) => $x ) ( (M add (succ $x) $y) => (succ (M add $x $y))) ( (M min (zero) _) => (zero) ) ( (M min _ (zero) ) => (zero) ) ( (M min (succ $x) (succ $y)) => (succ (M min $x $y))) ( (M max (zero) $x) => $x ) ( (M max $x (zero) ) => $x ) ( (M max (succ $x) (succ $y)) => (succ (M max $x $y))) ))

(define (list->seq lst) (if (null? lst) '(seq-empty) `(seq ,(car lst) ,(list->seq (cdr lst))))) ;; Extract the nth element from a sequence of elements ;; nth(0,(t,_)) -> somestr(t) ;; nth(n,(_,l)) when n > 0 -> nth(n - 1,l) (define rule-seq `( ( (M nth (zero) (seq $h $t)) => $h ) ( (M nth (succ $n) (seq $h $t)) => (M nth $n $t) ) ,@rule-arith ))

(define term `(M nth ,(make-numeral 2) ,(list->seq '(a b c d)))) (reduce term rule-seq) => c

## About this egg

### Author

Oleg Kiselyov; adapted to Chicken Scheme by Ivan Raikov

### Version history

- 1.0
- Initial release

### License

This library is released in the public domain.