Reasoned Schemer (006) (Schemeからの)翻訳

nulloは見たまんま

(defrel (nullo x)
  (== '() x))

なんだけどじーっと見てるとわからなくなってきたり
これは#sとか#uとか返すやつ

pairoもやることは見たまんまなんだけど定義にはconsoを使う

(defrel (pairo p)
  (fresh (a d) (conso a d p)))

Is pairo recursive?

そうか、nulloが出てきたということは再帰が出てくるってことか

(define (singleton? l)
  (cond ((pair?l) (null? (cdr l)))
        (else #f)))

これは普通の関数

日本語にするのはあきらめた

ふむ

翻訳（最初の版）
関数を関係に翻訳するには、まずdefineをdefrelに置き換える。次に、ひとつひとつのcond行をunnestし、condをcondeに置き換える。#tは#sに、#fは#uにunnnestする。

elseを#tにしておくのは、ルールを減らしたい、くらいのことかな

翻訳したもの

(defrel (singletono l)
  (conde ((pairo l) 
          (fresh (d)
             (cdro l d)
             (nullo d)))
         (#s #u)))

#uの掟
トップレベルのゴールに#uがあるconde行は値に貢献しない

とか使って簡単にすると

(defrel (singletono l)
  (fresh (d)
    (cdro l d)
    (nullo d)))

論理脳になればこういう表現が先に出てくるんだろうな
っていうかこれくらいならSchemeで書いて翻訳するより自分で１から考えたほうが速いか
最初にSchemeで作ってから翻訳するっていう書き方を推奨しているわけではあるまい
同じことが書けるよ！って言いたいんだろう

caroとcdroをconsoで定義せよ

(defrel (caro p a)
  (fresh (d) (conso a d) p))
(defrel (cdro p d)
  (fresh (a) (conso a d) p))

でいいかな？
せっかく翻訳の手順教えてもらったのにこれっぽっちも生かしていませんが
いいのか？

kb84tkhrのブログ