chickadee » tree-rewrite

Outdated egg!

This is an egg for CHICKEN 4, the unsupported old release. You're almost certainly looking for the CHICKEN 5 version of this egg, if it exists.

If it does not exist, there may be equivalent functionality provided by another egg; have a look at the egg index. Otherwise, please consider porting this egg to the current version of CHICKEN.

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

reduce M-TERM RULESprocedure

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.

rewrite-map-tree TREE RULESprocedure

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.

rewrite-fold-tree RULES F INITprocedure

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.

rewrite-fold-tree-partial RULES F INITprocedure

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.

match-tree TREE1 TREE2 ENVprocedure

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.

unify-trees TREE1 TREE2 ENVprocedure

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.

substitute-vars TERM ENVprocedure

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.

substitute-vars-open TERM ENVprocedure

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.