Ex. 4.38
まだ amb 評価器が実装されていないので、図を描いて解くことにする。
人間がやるので、当然ツリーの枝刈りを実施する。 枝刈りが効果的になるように、なるべく条件の多い人物を左側にもってくる。
こんな感じ。解は5組ある。
Ex. 4.39
最初の問について。条件の順番を変えたからと言って、解が変化することはない。同じである。
あたりまえの感じだが、一応証明。
(証)
- プログラムは、ツリーを全部調べて、条件がすべてTRUEになる解を全部見つける。①
- 条件の順番を入れかえたプログラムを作った場合、このプログラムも、 ツリーを全部調べて、条件がすべてTRUEになる解を全部見つける。②
ここで、①と②の解は同じでないと仮定する。例えば①の解Aが②の解になっていないとする。
②の解でないということは、解Aは、②の順番でならんだ条件のうちのどれかでFALSEになるということである。しかし、順番を変えても、TRUEだった条件がFALSEに変わることはない(条件の交換則)、ので解Aは②の順番でならんだ条件の全てでTRUEである。仮定から矛盾する2つの結論が得られたので、この仮定は間違っている。①と②の解は同じである。
次の問いは、計算効率についてである
ここでの amb と require の並び
amb1 amb2 amb3 amb4 amb5 require1 require2 require3 require4 require5 require6 require7
こうなっている。この場合、条件の順番を変えたところで、枝刈りは発生しないので、探索するツリーの大きさは変わらない。なので、効率は変わらない。同じである。
なお、require1～require7の適用は、ANDと同じなので、しょっちゅう偽になる条件を上のほうにしたほうが若干効率が上がる。しかし、これはツリーの枝刈りとは関係ない話。
Ex. 4.40
今度は、ツリーの枝刈りをするよう工夫しろという問題である。
ツリーの枝刈りは、amb と require を入れ子にすれば実現できる。
amb1
require1
amb2
amb3
amb4
amb5
require2
require3
require4
require5
require6
require7
こうすると、require1 が失敗すると、require1以下の行は実行されずに amb1 がバックトラックする。つまり require1 の失敗時は、amb2～amb5 は探索を実施しない。これは require1 でツリーを枝刈りしたことになる。
なので、枝刈りをする効率のよいプログラムは、こんな風になる。
(define (multiple-dwelling)
(let ((fletcher (amb 1 2 3 4 5)))
(require (not (= fletcher 5)))
(require (not (= fletcher 1)))
(let ((cooper (amb 1 2 3 4 5)))
(require (not (= cooper 1)))
(require (not (= (abs (- fletcher cooper)))))
(let ((miller (amb 1 2 3 4 5)))
(require (> miller cooper))
(let ((baker (amb 1 2 3 4 5)))
(require (not (= baker 5)))
(let ((smith (amb 1 2 3 4 5)))
(require (not (= (abs (- smith flethcer)))))
(require (distinct? (list baker cooper fletcher miller smith)))
(list 'fletcher fletcher 'cooper cooper
'miller miller 'baker baker 'smith smith)))))))
amb と require だけ抜き出すと
amb of fletcher
require
require
amb of cooper
require
require
amb of miller
require
amb of baker
require
amb of smith
require
require
こんな感じになっている。
Ex. 4.41
方針: 2.2.3章のフィルタを使う。可能な居住リストを作って、条件でフィルターする。
居住リストというのは、こういうの
( (1 1 1 1 1) (1 1 1 1 2) (1 1 1 1 3) ... )
これを、...bakerさんは5階には住まない...などの条件でフィルタする。プログラムはこんな感じ
(define (filter ... p.66
(define (enumerate-tree ... p.67
(define (flatmap ... p.71
; リスト2つからペアのリストつくる
; (1 2) と (1 2) → ( (1 1) (1 2) (2 1) (2 2) )
(define (pairs lst1 lst2)
(map enumerate-tree
(flatmap (lambda (i) (map (lambda (j) (list i j)) lst1)) lst2)))
; 5以下の整数を4つ掛けて120になるのは 2*3*4*5 しかないので
(define (distinct? lst)
(and (= (apply * lst) 120)
(= (apply min lst) 1)))
;居住条件
(define (dwelling? x)
(let ((baker (car x))
(cooper (cadr x))
(fletcher (caddr x))
(miller (cadddr x))
(smith (car (cddddr x))))
(and (distinct? (list baker cooper fletcher miller smith))
(not (= baker 5))
(not (= cooper 1))
(not (= fletcher 5))
(not (= fletcher 1))
(> miller cooper)
(not (= (abs (- smith fletcher)) 1))
(not (= (abs (- fletcher cooper)) 1)))))
;居住リスト
(define dwelling-list
(pairs (pairs (pairs (pairs '(1 2 3 4 5) '(1 2 3 4 5))
'(1 2 3 4 5))
'(1 2 3 4 5))
'(1 2 3 4 5)))
;居住リストを居住条件でフィルタする
(filter dwelling? dwelling-list)
この問題の意図は、amb評価器は、ストリームを利用しても実装できるということである。4.3.3章では、継続を利用してamb評価器を実装している。しかし、この問題のように amb式をストリームに置き換えるようなamb評価器を作ることも可能な感じがする。実際、4.4章の質問システムはストリームで作っている。
Ex. 4.42
うその条件の表現は、条件を or でつなげばいいだけ。
(A or B) and (C or D)...とする。AとBはどちらかが本当でどちらかが嘘、CとDはどちらかが本当でどちらかが嘘、、、という風に。解は、(A or B)=TRUE 、 (C or D)=TRUE 、、、となるから、ちょうどうまく本当の条件だけを辿ってくる。
なお、require を縦にならべるのは、条件をANDでつないでいるのと同じこと。
プログラムは、
(let ((betty (amb 1 2 3 4 5))
(ethel (amb 1 2 3 4 5))
(joan (amb 1 2 3 4 5))
(kitty (amb 1 2 3 4 5))
(mary (amb 1 2 3 4 5)))
(require (or (= kitty 2) (= betty 3)))
(require (or (= ethel 1) (= joan 2)))
(require (or (= joan 3) (= ethel 5)))
(require (or (= kitty 2) (= mary 4)))
(require (or (= mary 4) (= betty 1)))
(list 'betty betty 'ethel ethel 'joan joan 'kitty kitty 'mary mary))
となる。なお各人が2つとも本当のことを言ったり、2つとも嘘を言ったりしないことは 問題文で保証されているから、プログラムではそれを考慮する必要はない。 むしろ、問題文が仕様とするなら、仕様通り、正確に、各人は1つの本当と1つの嘘を言うという前提でプログラムを作るべきである。
Ex. 4.43
いかに amb が高性能といえども、さすがに自然言語の問題文を、そのままプログラムに入力するわけにはいかない。やはり人間様がある程度整理してあげないといけない。
娘候補は5人いる、Mary, Gabrielle, Lorna, Rosalind, Melissa である。
父親候補も5人、Downing, Hall, Barnacle, Paker, Moor である。
"ヨットを持っている"というのは、プログラムに必要な条件ではない。 他にもいろいろ書かれているが、使う条件は、"一人づつ娘を持つこと"、"ヨットの名前" と "Moore父娘の苗字" の件だけである。
(let ((father-of-mary (amb 'downing 'hall 'barnacle 'paker 'moor))
(father-of-gabrielle (amb 'downing 'hall 'barnacle 'paker 'moor))
(father-of-lorna (amb 'downing 'hall 'barnacle 'paker 'moor))
(father-of-rosalind (amb 'downing 'hall 'barnacle 'paker 'moor))
(father-of-melissa (amb 'downing 'hall 'barnacle 'paker 'moor)))
(require (eq? father-of-mary 'moor))
(require (not (eq? father-of-gabrielle 'barnacle)))
(require (not (eq? father-of-lorna 'moor)))
(require (not (eq? father-of-rosalind 'hall)))
(require (not (eq? father-of-melissa 'downing)))
(require (eq? father-of-melissa 'barnacle))
(require (not (eq? father-of-gabrielle 'parker)))
(require (distinct? father-of-mary
father-of-gabrielle
father-of-lorna
father-of-rosalind
father-of-melissa)
(list 'father-of-lorna father-of-lorna))
問題文の最後の条件、"Gabrielleの父親はParker博士の娘の名前をつけたヨットを持つ"という条件についての説明、、、
とりあえず、そのまま書き下してみる。Parker博士の娘をAとして
(and (eq? father-of-A 'parker) (not (eq? father-of-A father-of-gabrielle)))
となる。A を娘5人で展開すると
(or (and (eq? father-of-mary 'parker) (not (eq? father-of-mary father-of-gabrielle)))
(and (eq? father-of-gabrielle 'parker) (not (eq? father-of-gabrielle father-of-gabrielle)))
(and (eq? father-of-lorna 'parker) (not (eq? father-of-lorna father-of-gabrielle)))
(and (eq? father-of-rosalind 'parker) (not (eq? father-of-rosalind father-of-gabrielle)))
(and (eq? father-of-melissa 'parker) (not (eq? father-of-melissa father-of-gabrielle))))
となる。これをこのままプログラムに組み込んでも良いが、少し整理してみる。
式をよく見ると、問題の他の条件や、恒等式により真偽が決まっている部分式がある。
(not (eq? father-of-mary father-of-gabrielle)) = TRUE ← 5人の父親は別々の娘を持つという条件より (not (eq? father-of-gabrielle father-of-gabrielle)) = FALSE ← 恒等式 ...
とかである。これらの真偽の決まった式をTRUE、FALSEと置き換えて整理すると、
(or (eq? father-of-mary 'parker)
(eq? father-of-lorna 'parker)
(eq? father-of-rosalind 'parker)
(eq? father-of-melissa 'parker))
となる。これは、Gabrielle以外の娘のうちの誰かの父親がParkerであるということである。 それは、即ち、Gabrielleの父親はParkerではないというのと同じことである。
(not (eq? father-of-gabrielle 'parker))
ということで、最終的にこの条件をプログラムの条件として使っている。
次に、プログラムの効率良くする。効率を良くするには、ツリーを枝刈りすることである。 枝刈りは amb と require を入れ子にして実現する。その際、なるべく効きそうな条件を上の方に持ってくると効果的である。
(let ((father-of-mary (amb 'downing 'hall 'barnacle 'paker 'moor)))
(require (eq? father-of-mary 'moor))
(let ((father-of-melissa (amb 'downing 'hall 'barnacle 'paker 'moor)))
(require (eq? father-of-melissa 'barnacle))
(require (not (eq? father-of-melissa 'downing)))
(let ((father-of-gabrielle (amb 'downing 'hall 'barnacle 'paker 'moor)))
(require (not (eq? father-of-gabrielle 'barnacle)))
(require (not (eq? father-of-gabrielle 'parker)))
(let ((father-of-lorna (amb 'downing 'hall 'barnacle 'paker 'moor))
(father-of-rosalind (amb 'downing 'hall 'barnacle 'paker 'moor)))
(require (not (eq? father-of-lorna 'moor)))
(require (not (eq? father-of-rosalind 'hall)))
(require (distinct? father-of-mary
father-of-gabrielle
father-of-lorna
father-of-rosalind
father-of-melissa)
(list 'father-of-lorna father-of-lorna)))))
Mary ann と Mooreの苗字が同じという条件が無い場合は、上のプログラムから
(require (eq? father-of-mary 'moor))
を削除すればよい。
Ex. 4.44
こまの座標を amb で表して、こまの置き場所の制限を require で書き下せばよい。
こまの置き場所の制限： ｘ 座標がバラバラであること。ｙ座標がバラバラであること。斜め座標１がバラバラであること。斜め座標2がバラバラであること。の4つ
(let ((queen1-x (amb 1 2 3 4 5 6 7 8))
(queen1-y (amb 1 2 3 4 5 6 7 8))
(queen2-x (amb 1 2 3 4 5 6 7 8))
(queen2-y (amb 1 2 3 4 5 6 7 8))
(queen3-x (amb 1 2 3 4 5 6 7 8))
(queen3-y (amb 1 2 3 4 5 6 7 8))
(queen4-x (amb 1 2 3 4 5 6 7 8))
(queen4-y (amb 1 2 3 4 5 6 7 8))
(queen5-x (amb 1 2 3 4 5 6 7 8))
(queen5-y (amb 1 2 3 4 5 6 7 8))
(queen6-x (amb 1 2 3 4 5 6 7 8))
(queen6-y (amb 1 2 3 4 5 6 7 8))
(queen7-x (amb 1 2 3 4 5 6 7 8))
(queen7-y (amb 1 2 3 4 5 6 7 8))
(queen8-x (amb 1 2 3 4 5 6 7 8))
(queen8-y (amb 1 2 3 4 5 6 7 8)))
(require (distinct? queen1-x queen2-x queen3-x queen4-x
queen5-x queen6-x queen7-x queen8-x))
(require (distinct? queen1-y queen2-y queen3-y queen4-y
queen5-y queen6-y queen7-y queen8-y))
(require (distinct? (+ queen1-x queen1-y) (+ queen2-x queen2-y)
(+ queen3-x queen3-y) (+ queen4-x queen4-y)
(+ queen5-x queen5-y) (+ queen6-x queen6-y)
(+ queen7-x queen7-y) (+ queen8-x queen9-y)))
(require (distinct? (- queen1-x queen1-y) (- queen2-x queen2-y)
(- queen3-x queen3-y) (- queen4-x queen4-y)
(- queen5-x queen5-y) (- queen6-x queen6-y)
(- queen7-x queen7-y) (- queen8-x queen9-y)))
(list (list queen1-x queen1-y)(list queen2-x queen2-y)
(list queen3-x queen3-y)(list queen4-x queen4-y)
(list queen5-x queen5-y)(list queen6-x queen6-y)
(list queen7-x queen7-y)(list queen8-x queen8-y)))
斜め座標は、
斜め座標1 = x + y 斜め座標2 = x - y
となる。式の形は、45°回転の座標変換だが、図をみればそんな解釈も特に必要ない。
もっと大きい盤にしたい場合は、Ex. 4.35(p.248)で作った an-integer-between を使って
... (queen1-x (an-integer-between 1 30)) (queen1-y (an-integer-between 1 30)) ...
などどすればよい。なお、クィーンのこまの数は8個固定で、盤が大きくなってもこまの数は増やす必要はない。
あと、上のプログラムでｘ座標、y座標、斜め座標1、斜め座標2の条件を別々に固めてしまっているが、これで大丈夫なのか？ということについて、、、
エイトクィーンのルールの通りに条件を書き下すと、(こまの数を3つに減らして書く)
こうなる。一方、プログラムで使った条件を書き下すと
となる。エイトクィーンの条件は重複した部分があるので、それを整理すると、プログラムで使った条件と同じになる。