(wat-aro)

生きてます

SICP 問題 4.68

(define (my-reverse lst)
  (let iter ((lst lst) (result '()))
    (if (null? lst)
        result
        (iter (cdr lst) (cons (car lst) result)))))

(rule (append-to-form () ?y ?y))
(rule (append-to-form (?u . ?v) ?y (?u . ?z))
      (append-to-form ?v ?y ?z))

(reverse (?x) (?x))は当然成り立つ.
(?x . ?y) ?zの関係で考える.
?zの末尾は(?x)なので
(append something (?x) ?z)
somethingは残った?yをreverseしたものなので
(reverse ?y something)
規則として書いてみると

(rule (reverse (?x) (?x)))

(rule (reverse (?x . ?y) ?z)
      (and (append-to-form ?something ?x ?z)
           (reverse ?y ?something)))

実際にリストを入れて確かめてみる.
(reverse (1 2 3 4) ?z)
まず,appendで(append-to-form ?something (1) ?z)となる.
次の行で(reverse (2 3 4) ?something)
appendに進み(append-to-form ?something2 (2) ?something)
(reverse (3 4) ?something2)
appendにいき(append-to-form ?something3 (3) ?something2)
(reverse (4) ?something3)
ひとつ目の定義から
?something3 = (4)

(append-to-form ?something3 (3) ?something2)なので
?something2 = (4 3)

(append-to-form ?something2 (2) ?something)なので
?something = (4 3 2)

(append-to-form ?something (1) ?z)なので
?z = (4 3 2 1)

これでうまくいくはず.

次は逆を考えてみる.
(reverse (?x . ?y) (1 2 3 4))
(and (append-to-form ?something ?x ?z))
候補は(append (1 2 3 4) '())(append (1 2 3) (4)) (append (1 2) (3 4)) (append (1) (2 3 4))(append-to-form () (1 2 3 4))
ここで?x = ()とすると
?somethingは(1 2 3 4)
(reverse ?y (1 2 3 4))
ここで?z = (1 2 3 4)と同じになるので無限ループになる.
他のルートから進んでもかならずこのパターンもチェックするので無限ループは避けられない.