EoPL reading (29) 1.3.1 Free and Bound Variables

scheme EoPL

昨晩爆呑。芋焼酎のロックを水割りと勘違いしてガブ呑み。さすがに帰宅後に、は無理でした。そりゃいいとして試験の検討続行。
ええと、occurs-bound? の考え方てきには

  • exp が '() なら #f を戻す
  • exp が symbol なら #f を戻す
  • (car exp) が 'lambda なら
    • lambda body が occurs bound なら #t を戻す
    • lambda body が occurs bound でないなら
      • 引数の要素と var が同じ
      • かつ (cddr exp) が occurs free なら #t を戻す
  • 上記いずれでも無い場合、car 又は cdr 要素が occurs bound なら #t を戻す。どちらも #f なら #f を戻す

という事になるんですが、既に書いてる試験でカバーしてるのかどうか不明。現時点での試験が以下です。まず、occurs-free? な試験。

(use gauche.test)

(add-load-path ".")
(load "occurs-free-bound")

(test-start "occurs-free")
(test-section "ut")
;; E is a variable reference and E is the same as x
(test* "(occurs-free? 'x 'x) should return #t"
       #t
       (occurs-free? 'x 'x))

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

;; E is of the form (lambda (y) E), where y is different from x
;; and x occurs free in E'
(test* "(occurs-free? 'x '(lambda (y) ())) should return #f"
       #f
       (occurs-free? 'x '(lambda (y) ())))
(test* "(occurs-free? 'x '(lambda (y) x)) should return #t"
       #t
       (occurs-free? 'x '(lambda (y) x)))
(test* "(occurs-free? 'x '(lambda (y) y)) should return #f"
       #f
       (occurs-free? 'x '(lambda (y) y)))
(test* "(occurs-free? 'x '(lambda (x) x)) should return #f"
       #f
       (occurs-free? 'x '(lambda (x) x)))

(test* "(occurs-free? 'x '(lambda (a b c) ())) should return #f"
       #f
       (occurs-free? 'x '(lambda (a b c) ())))
(test* "(occurs-free? 'x '(lambda (a b c) x)) should return #t"
       #t
       (occurs-free? 'x '(lambda (a b c) x)))
(test* "(occurs-free? 'x '(lambda (a b c) y)) should return #f"
       #f
       (occurs-free? 'x '(lambda (a b c) y)))
(test* "(occurs-free? 'x '(lambda (v w x) x)) should return #f"
       #f
       (occurs-free? 'x '(lambda (v w x) x)))

(test* "(occurs-free? 'x '(lambda (y) (a b c))) should return #f"
       #f
       (occurs-free? 'x '(lambda (y) (a b c))))
(test* "(occurs-free? 'x '(lambda (y) (v w x))) should return #t"
       #t
       (occurs-free? 'x '(lambda (y) (v w x))))
(test* "(occurs-free? 'x '(lambda (x) x)) should return #f"
       #f
       (occurs-free? 'x '(lambda (x) (v w x))))

(test* "(occurs-free? 'x '(lambda (a b c) (a b c))) should return #f"
       #f
       (occurs-free? 'x '(lambda (a b c) (a b c))))
(test* "(occurs-free? 'x '(lambda (a b c) (v w x))) should return #t"
       #t
       (occurs-free? 'x '(lambda (a b c) (v w x))))
(test* "(occurs-free? 'x '(lambda (v w x) (v w x))) should return #f"
       #f
       (occurs-free? 'x '(lambda (v w x) (v w x))))

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

(test-end)

で、問題の occurs-bound? な試験が以下。

(use gauche.test)

(add-load-path ".")
(load "occurs-free-bound")

(test-start "occurs-bound")
(test-section "ut")
(test* "(occurs-bound? 'x ()) should return #f"
       #f
       (occurs-bound? 'x ()))
(test* "(occurs-bound? 'x 'x) should return #f"
       #f
       (occurs-bound? 'x 'x))

;; E is of the form (lambda (y) E), where x occurs bound in E'
;; or x and y are the same variable and y occurs free in E'

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

;; (not (occurs-bound? 'x '(x)))
(test* "(occurs-bound? 'x '(lambda (x y z) x)) should return #t"
       #t
       (occurs-bound? 'x '(lambda (x y z) x)))
;; (not (occurs-bound? 'x '(y)))
(test* "(occurs-bound? 'x '(lambda (x y z) y)) should return #f"
       #f
       (occurs-bound? 'x '(lambda (x y z) y)))
;; (not (occurs-bound? 'x '(x)))
(test* "(occurs-bound? 'x '(lambda (a b c) x)) should return #f"
       #f
       (occurs-bound? 'x '(lambda (a b c) x)))

;; (not (occurs-bound? 'x '(x y z)))
(test* "(occurs-bound? 'x '(lambda (x) (x y z)) should return #t"
       #t
       (occurs-bound? 'x '(lambda (x) (x y z))))
;; (not (occurs-bound? 'x '(y x z)))
(test* "(occurs-bound? 'x '(lambda (x) (y x z)) should return #t"
       #t
       (occurs-bound? 'x '(lambda (x) (y x z))))
;; (not (occurs-bound? 'x '(y z x)))
(test* "(occurs-bound? 'x '(lambda (x) (y z x)) should return #t"
       #t
       (occurs-bound? 'x '(lambda (x) (y z x))))
;; (not (occurs-bound? 'x '(a b c)))
(test* "(occurs-bound? 'x '(lambda (x) (a b c))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (x) (a b c))))
;; (not (occurs-bound? 'x '(x y z)))
(test* "(occurs-bound? 'x '(lambda (y) (x y z))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (x y z))))

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

;; (occurs-bound? 'x '(lambda (x y z) x))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x y z) x))) should return #t"
       #t
       (occurs-bound? 'x '(lambda (y) (lambda (x y z) x))))
;; (not (occurs-bound? 'x '(lambda (x y z) y)))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x y z) y))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (lambda (x y z) y))))
;; (not (occurs-bound? 'x '(lambda (a b c) x)))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (a b c) x))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (lambda (a b c) x))))

;; (occurs-bound? 'x '(lambda (x) (x y z)))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x) (x y z)))) should return #t"
       #t
       (occurs-bound? 'x '(lambda (y) (lambda (x) (x y z)))))
;; (occurs-bound? 'x '(lambda (x) (y x z)))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x) (y x z)))) should return #t"
       #t
       (occurs-bound? 'x '(lambda (y) (lambda (x) (y x z)))))
;; (occurs-bound? 'x '(lambda (x) (y z x)))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x) (y z x)))) should return #t"
       #t
       (occurs-bound? 'x '(lambda (y) (lambda (x) (y z x)))))
;; (not (occurs-bound? 'x '(lambda (x) (a b c))))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (x) (a b c)))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (lambda (x) (a b c)))))
;; (not (occurs-bound? 'x '(lambda (y) (x y z))))
(test* "(occurs-bound? 'x '(lambda (y) (lambda (y) (x y z)))) should return #f"
       #f
       (occurs-bound? 'x '(lambda (y) (lambda (y) (x y z)))))

(test-end)

コメントが微妙ですがご容赦願います。今からカバレッジ具合を検証。

続き

ええと、(cddr exp) が occurs bound でないケイスの式を以下に列挙してみます。以下の式が occurs-free であれば #t が戻る。

  • (lambda (x) ()) ;; not occurs free
  • (lambda (x) y) ;; not occurs free
  • (lambda (y) x)) ;; occurs free
  • (lambda (x y z) y) ;; occurs free
  • (lambda (a b c) x) ;; occurs free but
  • (lambda (x) (a b c)) ;; not occurs free
  • (lambda (y) (x y z)) ;; not occurs free

あら、結構少ないな。よく手続きを見てみるに、occurs bound ではなく、occurs free な式 (そうでないものも含む) の試験をきちんとヤッてるかどうか。
スデにカバー済みかどうかも微妙。あ、以下は少なくとも漏れてますね。

(lambda (x y z) a)

とか

(lambda (x) (x y z))

あ、下の方はそれ以前に occurs-bound? で #t になるのか。上側も微妙。まだ occurs-bound? の仕様をきちんと理解できてないな。(とほほ