Reasoned Schemer (005) caro、cdro、conso

Don't put new wine into old bottlesのもじりだったりするんだろうか
あんまり関係ないかな
そういうとこ気にしなきゃいけないとこが多そうで翻訳はちょっとたいへんそうだな
SICPとかマジメなやつのほうがある意味楽そう

さてcarの論理版？caroというのが出てきます
(run* q (caro '(a c o r n) q))とやるとqが'aになるという

定義

(defrel (caro p a)
  (fresh (d)
    (== (cons a d) p)))

pのcarがaである、とは
aと何かをconsするとpになる、ということである
と読めばいいかな

あんまり意識してなかったけど関数も普通に使えるんだな
carとcaroを混乱しないようにしないと

(car (cdr (cdr '(a c o r n))))といった式を関係型に書き直すときに
中間的な変数を使って入れ子を外していくことをunnestingといいます

(run* r
  (fresh (v)
    (cdro '(a c o r n) v)
    (fresh (w)
      (cdro v w)
      (caro w r))))

こうでもいいのかな？

(run* r
  (fresh (v w)
    (cdro '(a c o r n) v)
    (cdro v w)
    (caro w r)))

なんかダメな理由あったっけ・・・？

cdro、consoも出てきて

(caro p a) pのcarはa
(cdro p d) pのcdrはd
(conso a d p) aとdのconsはp

結果が右に来る、っていうのがお作法なんだなきっと

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

caroとconsoはconsで定義して、consoはcaroとcdroで定義している
consoをconsで定義することはできないのかな？
と思ったらこういう定義も書かれている

(defrel (conso a d p)
  (== `(,a . ,d) p))

突然のドット記法
当然こうも書けるはず

(defrel (conso a d p)
  (== (cons a d) p))

caroやcdroだってcarやcdrで書けるはずか・・・

(defrel (caro p a) (== (car p) a))
(defrel (cdro p d) (== (car p) d))

caroやcdroをconsで書いて、
consoをcaroやcdroで書いてるのは、
できるだけSchemeの関数に依存しないように、ってことかな
consが基礎中の基礎ってことになるんだろうか
なにせ偉大なるcons様だからな

oはなんの意味かと思ってたけど、単にSchemeの関数と見分けるためだけのものかもしれないなあ
なにに由来しているのかはわからない

kb84tkhrのブログ