定理証明手習い (62) C 小さなお手伝い
付録CはJ-Bob自体の定義と解説です
本編にはYコンビネータとか継続渡しとかインタプリタみたいな中ボス大ボスがいなかったので
ここがそういう位置づけになるのかもしれません
ソースはダウンロード済みですが自分で打ち込みながら進めようと思います
全ソースコードが載ってるかどうかは微妙に不安
読者のみなさんも、できれば好きな言語でJ-Bobとその言語を実装してみてください。
J-Bobの組み込み関数さえ互換性のある形で実装できればあとは同じコードでいけるはずだしね
Racketで書いてみようかなと思いましたがRacketでは組み込み関数の上書きが許されていないので
単純な形では実装できなさそうでここはあきらめておきます
RacketでACL2が書いてあるほどなのでできないわけではないはずですがちょっと大掛かりに
なるんじゃないかと
Readerをいじったりとか
ごく単純な言語なので、Scheme修行のインタプリタを手直しして使うとかすると面白いかもしれませんね?
Scheme手習いのインタプリタはdefine
すらないのでさすがに不足なのが明らか
というわけなので
SchemeでJ-Bobを使うには
ACL2の方ではなくてこっちでいきます