1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
;;; -*-Scheme-*-
;;;
;;; From Kent Dybvig's book on Chez Scheme
(define unify)
(letrec
((occurs?
(lambda (u v)
(and (pair? v)
(define (f l)
(and (not (null? l))
(or (eq? u (car l))
(occurs? u (car l))
(f (cdr l)))))
(f (cdr v)))))
(sigma
(lambda (u v s)
(lambda (x)
(define (f x)
(if (symbol? x)
(if (eq? x u) v x)
(cons (car x) (map f (cdr x)))))
(f (s x)))))
(try-subst
(lambda (u v s ks kf)
(let ((u (s u)))
(if (not (symbol? u))
(uni u v s ks kf)
(let ((v (s v)))
(cond
((eq? u v) (ks s))
((occurs? u v) (kf "loop"))
(else (ks (sigma u v s)))))))))
(uni
(lambda (u v s ks kf)
(cond
((symbol? u) (try-subst u v s ks kf))
((symbol? v) (try-subst v u s ks kf))
((and (eq? (car u) (car v))
(= (length u) (length v)))
(define (f u v s)
(if (null? u)
(ks s)
(uni (car u)
(car v)
s
(lambda (s) (f (cdr u) (cdr v) s))
kf)))
(f (cdr u) (cdr v) s))
(else (kf "clash"))))))
(set! unify
(lambda (u v)
(uni u
v
(lambda (x) x)
(lambda (s) (s u))
(lambda (msg) msg)))))
(print (unify 'x 'y))
(print (unify '(f x y) '(g x y)))
(print (unify '(f x (h)) '(f (h) y)))
(print (unify '(f (g x) y) '(f y x)))
(print (unify '(f (g x) y) '(f y (g x))))
|
