Untitled
unknown
plain_text
2 months ago
2.7 kB
7
Indexable
'(Testing the substitute) ; 1) Is x in list? (fun in? (x ()) () (x (y . ys)) (if (equal x y) 'T (in? x ys))) ; 2) Remove elements of B from A (fun difference (() B) () ((a . as) B) ( if (in? a B) (difference as B) (:: a (difference as B))) ) (fun free-vars ; If the term is (quote e), strip off quote and recurse ((quote e)) (free-vars e) ; If the term is a pair (head . tail) ((head . tail)) (if (equal head '\) ; If head = '\, handle a multi-parameter lambda (handle-lambda tail) ; Otherwise, gather free vars from both (append (free-vars head) (free-vars tail))) ; If it’s a bare symbol, return (x), else empty (x) (if (symbol? x) (list x) ()) ) ; handle-lambda expects tail to be ( (p1 p2 ...) . (body . ()) ) (fun handle-lambda ((params . (body . ()))) (difference (free-vars body) params) (anything) () ) (free-vars '(\ (x) (x y))) (free-vars '(\ (x y) (x y))) (free-vars '(\ () (x y))) ; 2) fresh2: helper to pick a fresh variable ; If no candidates left, return 'NoFreshVariables instead of throwing an error. (fun fresh2 (avoid ()) 'NoFreshVariables (avoid (cand . cands)) (if (in? cand avoid) (fresh2 avoid cands) cand)) ; 3) fresh: picks a fresh variable not in AVOID from a fixed list (fun fresh (avoid) (fresh2 avoid '(a b c d e f g h i j k l m n o p q r s t u v w x y z))) (fresh '(x y z)) (fresh '(a b c d e f g h i j k l m n o p q r s t u v w x y z)) (fun substitute ; If the term is (quote e), unwrap and recurse ((quote e) x t2) (substitute e x t2) ; 3) If term is an application (t3 . t4), ; build a 2-element list: (sub(t3) sub(t4)) ((t3 . t4) x t2) (:: (substitute t3 x t2) (substitute t4 x t2)) ; 4) If term is a lambda (\ (y) body), ; do alpha-conversion if y is in free-vars(t2)+free-vars(body). ((\ (y) body) x t2) (if (equal x y) (\ (y) body) (let fvT2 (free-vars t2) (let fvBody (free-vars body) (let avoid (append fvT2 fvBody) (if (in? y avoid) (let z (fresh avoid) (\ (z) (substitute (substitute body y z) x t2))) (\ (y) (substitute body x t2))))))) ; 1) If term is exactly x, replace it with t2 (term x t2) (if (equal term x) t2 term) ; 2) If term is a symbol, keep it ((? symbol? term) x t2) term ; 5) Numbers or anything else (term x t2) term) ; Test (substitute '((\ x (x y)) y) 'y 'z)
Editor is loading...
Leave a Comment