kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

Reasoned Schemer (77) defrel 続きとconde

> (run* (x y) (teacupo x) (teacupo y))
'((tea tea) (tea cup) (cup tea) (cup cup))

こうやって組み合わせで増えていくのがrelationalっぽいような気がする

追っかける・・・
ちょっとめんどそうだなあ

> (((((conj2 (teacupo x) (teacupo y)) empty-s))))
'(((#(y) . tea) (#(x) . tea))
  ((#(y) . cup) (#(x) . tea))
  ((#(y) . tea) (#(x) . cup))
  ((#(y) . cup) (#(x) . cup)))

3回forceしてやっと答えが出る

defrelの定義からlambda ()を取ってみた

(define-syntax defrel
  (syntax-rules ()
    ((defrel (name x ...) g ...)
     (define (name x ...)
       (lambda (s) ((conj g ...) s))))))

普通に動くな

> (run* (x y) (teacupo x) (teacupo y))
'((tea tea) (tea cup) (cup tea) (cup cup))

困るまでこのdefrelで進んでみようか
それはそれで忘れて困りそうだけど

できるところまでやってみる

  (take-inf #f ((conj2 (teacupo x) (teacupo y)) empty-s))
= (take-inf #f (append-map-inf (teacupo y) ((teacupo x) empty-s)))
= (take-inf #f (append-map-inf (teacupo y) (lambda () ((disj2 (== 'tea x) (== 'cup x)) empty-s))))
= (take-inf #f (append-map-inf (teacupo y) ((disj2 (== 'tea x) (== 'cup x)) empty-s)))
= (take-inf #f (append-map-inf (teacupo y) `(((,x . tea)) ((,x . cup)))))
= (take-inf #f (append-inf ((teacupo y) `((,x . tea)))
                 (append-map-inf (teacupo y) `(((,x . cup))))))
= (take-inf #f (append-inf ((teacupo y) `((,x . tea))) 
                 (append-inf ((teacupo y) `((,x . cup))) '())))
= (take-inf #f (append-inf (lambda () ((disj2 (== 'tea y) (== 'cup y)) `((,x . tea))))
                 (append-inf (lambda () ((disj2 (== 'tea y) (== 'cup y)) `((,x . cup)))) '())))
= (take-inf #f (append-inf (lambda () ((disj2 (== 'tea y) (== 'cup y)) `((,x . tea))))
                 (append-inf '() ((disj2 (== 'tea y) (== 'cup y)) `((,x . cup))))))
= (take-inf #f (append-inf (lambda () ((disj2 (== 'tea y) (== 'cup y)) `((,x . tea))))
                 ((disj2 (== 'tea y) (== 'cup y)) `((,x . cup)))))
= (take-inf #f (append-inf (lambda () ((disj2 (== 'tea y) (== 'cup y)) `((,x . tea))))
                 `(((,y . tea) (,x . cup)) ((,y . cup) (,x . cup)))))
= (take-inf #f (append-inf `(((,y . tea) (,x . cup)) ((,y . cup) (,x . cup)))
                 ((disj2 (== 'tea y) (== 'cup y)) `((,x . tea)))))
= (take-inf #f (append-inf `(((,y . tea) (,x . cup)) ((,y . cup) (,x . cup)))
                 `(((,y . tea) (,x . tea)) ((,y . cup) (,x . tea)))))
= (take-inf #f `(((,y . tea) (,x . cup)) ((,y . cup) (,x . cup))
                 ((,y . tea) (,x . tea)) ((,y . cup) (,x . tea))))
= `(((,y . tea) (,x . cup)) ((,y . cup) (,x . cup))
    ((,y . tea) (,x . tea)) ((,y . cup) (,x . tea)))

できた
ふう
append-infがforceしてるところは初めてまじめに追ったかな
でもまだdefrelの謎は解けない

あとはconde

> (run* (x y)
    (disj2 (conj2 (teacupo x) (teacupo x))
           (conj2 (== #f x) (teacupo y))))
'((tea _0) (cup _0) (#f tea) (#f cup))

> (run* (x y)
    (conde ((teacupo x) (teacupo x))
           ((== #f x) (teacupo y))))
'((tea _0) (cup _0) (#f tea) (#f cup))

と書ける
condeマクロのおかげ

(define-syntax conde
  (syntax-rules ()
    ((conde (g ...) ...)
     (disj (conj g ...) ...))))

1章おわり