EoPL reading (24) 1.3.1 Free and Bound Variables

scheme EoPL

occurs bound な UT を書く。
ええと、まず定義が無いので以下は両方 occurs bound ではない、という事になる。

(test* "(occurs-bound? 'x 'x) should return #f"
       #f
       (occurs-bound? 'x 'x))
(test* "(occurs-bound? 'x 'y) should return #f"
       #f
       (occurs-bound? 'x 'y))

次は lambda 式です。occurs bound の定義 1. によれば

  • E は (lambda (y) E') な式で E' に x が occurs bound しているか
  • x と y が同一の変数であり、かつ y が E' の中で occurs free

という記述になっております。定義の上側は E' な body が lambda 式の場合の定義になるのでしょうか。あるいは下側は記述的になんとなく微妙。手続きの定義を見るに

;; E is of the form (lambda (y) E'),
     ((eqv? (car exp) 'lambda)
;; where x occurs bound in E'
      (or (occurs-bound? var (caddr exp))
;; or x and y are the same variable
	  (and (eqv? (caadr exp) var)
;; and y occurs free in E'
	       (occurs-free? var (caddr exp)))))

という事になるのか。ちょっと記述的に微妙じゃね? と思いつつも手続き見て書いた試験が以下。

;; x and y are the same variable and y occurs free in E'
(test* "(occurs-bound? 'x '(lambda (x) x)) should return #t"
       #t
       (occurs-bound? 'x '(lambda (x) x)))

;; x and y are not the same variable
(test* "(occurs-bound? 'x '(lambda (y) x)) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) x)))

;; x and y are the same variable and y doesn't occurs free in E'
(test* "(occurs-bound? 'x '(lambda (x) y)) should return #f"
       #f
       (occurs-bound? 'x '(lambda (x) y)))

;; x doesn't occurs bound in E'
(test* "(occurs-bound? 'x '(lambda (y) (lambda (y) x))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (lambda (y) x))))

;; x doesn't occurs bound in E'
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x) y))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (lambda (x) y))))

;; x occurs bound in E'
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x) x))) should return #t"
       #t
       (occurs-bound? 'x '(lambda (y) (lambda (x) x))))

よく考えたら occurs-free? も occurs-bound? も

E is of the form (E1 E2) and x occurs {bound, free} in E1 or E2

というケイスの試験をしてないかも。以下?

(test* "(occurs-bound? 'x '(f x)) should return #f"
       #f
       (occurs-bound? 'x '(f x)))
(test* "(occurs-bound? 'x '((lambda (x) x) y) should return #t"
       #t
       (occurs-bound? 'x '((lambda (x) x) y)))
(test* "(occurs-bound? 'x '((lambda (y) y) x)) should return #f"
       #f
       (occurs-bound? 'x '((lambda (y) y) x)))

ちょっと巻き戻して occurs-free? も上記な試験を書いてみます。
以下ですが、まだ occurs free は若干不思議なカンジ。

;; 定義が無くても式に x が出てきたら occurs free
(test* "(occurs-free? 'x '(f x)) should return #t"
       #t
       (occurs-free? 'x '(f x)))

;; 定義もなくて式に x が出てこない場合は occurs free ではない
(test* "(occurs-free? 'x '(f y)) should return #f"
       #f
       (occurs-free? 'x '(f y)))

;; 定義があるので occurs free ではない
(test* "(occurs-free? 'x '((lambda (x) x) y)) should return #f"
       #f
       (occurs-free? 'x '((lambda (x) x) y)))

;; lambda 式は上記の通りダウトですが、式中に x あり
(test* "(occurs-free? 'x '((lambda (x) x) x)) should return #t"
       #t
       (occurs-free? 'x '((lambda (x) x) x)))

;; lambda 式が occurs free
(test* "(occurs-free? 'x '((lambda (y) x) y)) should return #t"
       #t
       (occurs-free? 'x '((lambda (y) x) y)))

;; x がどこにも出てこないので NG
(test* "(occurs-free? 'x '((lambda (y) y) y)) should return #f"
       #f
       (occurs-free? 'x '((lambda (y) y) y)))

む。((lambda (y) y) x) はおそらくビンゴだな。

(test* "(occurs-free? 'x '((lambda (y) y) x)) should return #t"
       #t
       (occurs-free? 'x '((lambda (y) y) x)))

当たり。occurs free だの occurs bound だののナニが随分見えるようになったんですが、Ex.1-20 はできるかどうか。とりあえずアツい中昼寝突入。