問題4.13-4.15

試験めんどくさい。そして寒い。
あ、続きです。

4.13

環境にある記号の束縛を除去する特殊形式unbind!を実装せよとのことです。仕様も自分で決めるらしいです。
例えば、現在のスコープでxが束縛されていなくて、その一つ上位のスコープでxが束縛されていた場合、(unbind! x)はどのような振る舞いをするのがふさわしいのか。あるいは、現在のスコープでxが3に束縛されていて、一つ上位のスコープではxが5に束縛されている場合はどうすればいいのか。とか。
後者の場合は、現在のスコープのみを除去するほうが、Schemeとしては自然なんじゃないかなと思います。現スコープのxと一つ上位のxは別物と考えたほうがたぶん気持ち悪くないです。
前者の場合は、環境モデルにのっとって自然に考えるなら、上位のxをunbind!しちゃうように実装するのがいいように思います。set!も

> (define x 3)
> (define (f y) (set! x y))
> (f 5)
> x
5

このように、一つ上位にあるxの変更を行うようになっているのが分かるので、これと同じようにunbind!も実装していいような気がします。ただ、

> (define x 3)
> (define (f y) (unbind! x) y)
> (f 10)
10
> x

のような場合を考えると、バグが入り込みやすい構造になってしまうようにも感じます。でも結局のところset!だって同じようなもんだし、unbind!だって!がついてるんだから破壊的代入のように腫れ物のように扱うような実装でいいんじゃないかな。などと考えたので、そのように実装します。

まず、いつものように述語と選択子を作ります。

(define (unbinder? exp) (tagged-list? exp 'unbind!))
(define (unbinder-variable exp) (cadr exp))

で、先日抽象したscan-frameを使います。

(define (unbind-variable! var env)
  (define (env-loop env)
    (scan-frame env
                var
                (lambda (x) (env-loop (enclosing-environment x)))
                (lambda (x) (delete-binding-from-frame! var (first-frame env)))))
  (env-loop env))

delete-binding-from-frame!はframe中のvarの束縛を除去します。ちょっと鈍くさいですが、次のようにします。

(define (delete-binding-from-frame! var frame)
  (define (delete-index var vars n)
    (if (eq? var (car vars))
        n
        (delete-index var (cdr vars) (+ n 1))))
  (define (delete-item-from-list lst n)
    (if (= n 0)
        (cdr lst)
        (cons (car lst) (delete-item-from-list (cdr lst) (- n 1)))))
  (let ((n (delete-index var (car frame) 0)))
    (set-car! frame (delete-item-from-list (car frame) n))
    (set-cdr! frame (delete-item-from-list (cdr frame) n))))

加えるのに比べるとやっぱり手間がかかりますね。もっとうまい方法があると思うけど、とりあえずこれでいいや。
あとはevalに次を加えます。

...
((unbinder? exp) (eval-unbind exp env))
...

eval-unbindは最初に定義した選択子を使って次のようにします。

(define (eval-unbind exp env)
  (unbind-variable! (unbinder-variable exp) env)
  'ok)

以上でunbind!を使う準備ができました。実際に動かしてみます。

;;; M-Eval input:
(define x 3)
;;; M-Eval value:
ok

;;; M-Eval input:
(unbind! x)
;;; M-Eval value:
ok

;;; M-Eval input:
x
Unbound variable x

;;; M-Eval input:
(define x 3)
;;; M-Eval value:
ok

;;; M-Eval input:
(define (f n)
  (define x 5)
  (unbind! x)
  n)
;;; M-Eval value:
ok

;;; M-Eval input:
(f 10)
;;; M-Eval value:
10

;;; M-Eval input:
x
;;; M-Eval value:
3

ということで、unbind!が実装できました。でもunbind!って実際どういう時に使うんですかね。あんまり使いどころがない気がします。

4.14

とりあえず1引数手続きのmapをdriver-loop上で作ってみます。多引数だとapplyが必要なので。(いや、もしかしたらなくてもできるのかも。できないかも。)

;;; M-Eval input:
(define (map f lst)
  (if (null? lst)
      '()
      (cons (f (car lst)) (map f (cdr lst)))))
;;; M-Eval value:
ok

;;; M-Eval input:
(map (lambda (x) x) '(1 2 3 4 5))
;;; M-Eval value:
(1 2 3 4 5)

;;; M-Eval input:
(map (lambda (x) (* x x x x)) '(1 10 100))
;;; M-Eval value:
(1 10000 100000000)

動きますね。一方mapを基本手続きとして組み込むと、

;;; M-Eval input:
(map (lambda (x) x) '(1 2 3))
map: expects type <procedure> as 1st argument, given: 
(procedure (x) (x) (((#f #t false true car cdr cons null? list + - * / modulo = < > 
eq? not display newline map) #f #t #f #t (primitive #<primitive:car>) 
(primitive #<primitive:cdr>) (primitive #<primitive:cons>) (primitive #<primitive:null?>) 
(pr...; other arguments were: (1 2 3)

こんなんが出ます。よく分からないのでググります。
基盤Schemeのmapは第一引数に通常の手続きをとりますが、今回作った評価器だと手続きの先頭にprocedureのタグが付きます(上のエラーを見ると分かります)。
そうすると、今回作った評価器では手続きとしてみなされるけれど、基盤Schemeではただのリストでしかないので、mapの第一引数がおかしいよーと基盤Schemeが怒ってしまうようです。ややこしいです。

4.15

停止性問題ですね。うーんこれでいいのかな。

背理法で証明します。
任意のp,aについて(p a)が停止するかどうかを判定できる述語halts?が存在すると仮定します。
すなわち、(halts? p a)は#tまたは#fを返します。
次のような一引数手続きf,
(define (f x)
  (if (halts? f x)
      (f x)
      x))
を作ります。zを何らかのオブジェクトとして、(f z)を評価した時のことを考えます。

(i)(halts? f z)=#tのとき、
halts?は停止判定を正しく行う述語と仮定したので、(f z)は停止するはずです。
しかし、(halts? f z)が真なので、定義から(f z)が停止しないことは明らか。矛盾。

(ii)(halts? f z)=#fのとき、
halts?は停止判定を正しく行う述語と仮定したので、(f z)は停止しないはず。
しかし、定義から(f z)はzを正しく返してくるので停止する。矛盾。

以上(i),(ii)から仮定は棄却されます。halts?は存在しません。

Turing Machineで証明するより面倒くさくないです。たぶん。いやそんなに変わらないかな。
Turing先生はすごいなぁと思います。

今日はここまで。