;;;; Rewriting ;;;; ND ;;;; Oct 2004 ;;;; ;;;; Handle nonlinearity Nov 2004 ;;;; ;;;; Innermost and outermost rewriting ;;;; Terms are s-expressions ;;;; Rules are dotted pairs (l . r) ;;;; Variables start with u,v,w,x,y,z ;;;; Systems are lists ;;;; (Substitutions are lists of dotted pairs) (define nil '()) (define (symbol->list x) (string->list (symbol->string x))) (define (atom? x) (or (null? x) (symbol? x) (number? x))) (define (var? x) ;; Is x a variable (start with u,v,w,x,y,z)? (and (symbol? x) (member (car (symbol->list x)) '(#\u #\v #\w #\x #\y #\z)))) (define (subst old new z) (cond ((null? z) nil) ((equal? old z) new) ((atom? z) z) (else (cons (subst old new (car z)) (subst old new (cdr z)))))) (define (subs s z) ;; Apply substitution s to z (if (null? s) z (subs (cdr s) (subst (caar s) (cdar s) z)))) (define (match? pat arg) ;; Does the pattern pat match the term arg? (cond ((var? pat) #t) ((atom? pat) (equal? pat arg)) ((atom? arg) #f) (else (and (match? (car pat) (car arg)) (match? (subs (match (car pat) (car arg)) (cdr pat)) (cdr arg)))))) (define (match pat arg) ;; Return substitution s such that s(pat)=arg (cond ((var? pat) (list (cons pat arg))) ((atom? pat) nil) ((atom? arg) nil) (else (append (match (car pat) (car arg)) (match (subs (match (car pat) (car arg)) (cdr pat) ) (cdr arg)))))) (define (rule r x) ;; Top rewrite of term x by rule r ;; Presumes match (subs (match (car r) x) (cdr r))) (define (tops s x) ;; Top rewrite of term x by system s (cond ((null? s) x) ((match? (caar s) x) (rule (car s) x)) (else (tops (cdr s) x)))) (define (redex? s x) ;; Is term x a redex of system s? (cond ((null? s) #f) ((match? (caar s) x) #t) (else (redex? (cdr s) x)))) (define (nf? s x) ;; Is term x a normal form of system s? (cond ((redex? s x) #f) ((atom? x) #t) ((redex? s (car x)) #f) (else (and (nf? s (car x)) (nf? s (cdr x)))))) (define (outer1 s x) ;; Outermost reduct of term x by system s (cond ((null? x) nil) ((redex? s x) (tops s x)) ((nf? s (car x)) (cons (car x) (outer1 s (cdr x)))) (else (cons (outer1 s (car x)) (cdr x))))) (define (outer s x) ;; Outermost normal form of term x by system s (if (nf? s x) x (outer s (outer1 s x)))) (define (inner s x) ;; Innermost normal form of term x by system s (cond ((nf? s x) x) ((symbol? x) (if (match? (caar s) x) (inner s (rule (car s) x)) (inner (cdr s) x))) (else (inner s (tops s (cons (inner s (car x)) (inner s (cdr x))))))))