Reasoned Schemer (003) conj2、disj2、defrel
conj2
はふたつのゴールが両方とも成功すれば成功する
2
は引数がふたつってこと
conjはたぶんconjunctionの略
連言てやつ andみたいなもの
定理証明手習いにも出てきた
disj2
はふたつのゴールのうちひとつでも成功すれば成功する
こっちはdisjunction 選言 orみたいなもの
fresh
やrun*
は複数の変数を取れる
(run* r
(fresh (x y)
(conj2 (conj2 (== 'split x)
(== 'pea y))
(== `(,x ,y) r))))
とか
(run* (r x y)
(conj2 (conj2 (== 'split x)
(== 'pea y))
(== `(,x ,y) r))))
とか
fresh
やrun*
は複数のゴールを持てる- そういう場合はゴールの連言として扱われる
let
に複数の式が書けるようなものか
- 関係に名前をつけるには
defrel
を使う
(defrel (teacupo t)
(disj2 (== 'tea t) (== 'cup t)))
teacupo
のo
はなんでしょうか
ていうかオーだよなこれ?本だとちょっとわかりづらい
オーはなんのオーだろう
上の定義は下の定義と同じらしい
(define (teacupo t)
(lambda (s)
(lambda ()
((disj2 (== 'tea t) (== 'cup t))
s))))
s
を引数にとってs
に(disj2 (== 'tea t) (== 'cup t))
を適用する
関数を返す関数
s
ってなんだろうな
disj2
はどんな関数を返すんだろう
うーんちょっとわからん
でとにかく定義すると(run* x (teacupo x))
みたいに使える
値は当然(tea cup)