kb84tkhrのブログ

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

Reasoned Schemer (86) nevero

今回のネタはこれ

(defrel (nevero) (nevero))

単純極まりない
でも1周目では腑に落ちないところがいくつかあった

失敗もしないし成功もしない、というのはいいとして
評価したら返ってこない、でもcondeでいろいろ探し続けてるみたい、どう動いてるの?
ってあたり
今はsuspensionのおかげで処理が返ってきてるんだろう、くらいはわかってる

> (run 1 q (nevero))

ここから見ていこう
わかるところから理解しておかないと後でわからなくなりそう

> ((nevero) empty-s)
#<procedure:...r/minikanren.rkt:147:9>
> (((nevero) empty-s))
#<procedure:...r/minikanren.rkt:147:9>
> ((((nevero) empty-s)))
#<procedure:...r/minikanren.rkt:147:9>

呼んだら返ってくるけど何度forceしてもsuspensionしか返ってこない

  ((nevero) empty-s)
= ((lambda (s) (lambda () (nevero s))) empty-s)
= (lambda () ((nevero) empty-s))

ここでいったんtake-infにもどってforceされる

  ((lambda () ((nevero) empty-s)))
= ((nevero) empty-s)

そういうことだよね

> (run 1 q fail (nevero))
'()

これはfail()を返すからappend-map-infneveroを呼ばない

> (run 1 q (conde (succeed) ((nevero))))
'(_0)
> (run 1 q (conde ((nevero)) (succeed)))
'(_0)

後者も止まらないのかと驚いた思い出
まず前者

> ((conde (succeed) ((nevero))) empty-s)
'(() . #<procedure:...r/minikanren.rkt:147:9>)
> ((cdr ((conde (succeed) ((nevero))) empty-s)))
#<procedure:...r/minikanren.rkt:147:9>
> (((cdr ((conde (succeed) ((nevero))) empty-s))))
#<procedure:...r/minikanren.rkt:147:9>

そんな感じだろうと思ってた
後者は1回forceした後同じになるのかな

> ((conde ((nevero)) (succeed)) empty-s)
#<procedure:...r/minikanren.rkt:56:10>
> (((conde ((nevero)) (succeed)) empty-s))
'(() . #<procedure:...r/minikanren.rkt:147:9>)
> ((cdr (((conde ((nevero)) (succeed)) empty-s))))
#<procedure:...r/minikanren.rkt:147:9>
> (((cdr (((conde ((nevero)) (succeed)) empty-s)))))
#<procedure:...r/minikanren.rkt:147:9>

正解
なお minikanren.rkt:56 はappend-infのdelay
ここで項が入れわかる

(define (append-inf s-inf t-inf)
  (cond
    ((null? s-inf) t-inf)
    ((pair? s-inf) (cons (car s-inf) (append-inf (cdr s-inf) t-inf)))
    (else (lambda () (append-inf t-inf (s-inf)))))) ; ここ

minikanren.rkt:147 はdefrelのdelay

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