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)