定理証明手習い (62) C 小さなお手伝い

付録CはJ-Bob自体の定義と解説です
本編にはYコンビネータとか継続渡しとかインタプリタみたいな中ボス大ボスがいなかったので
ここがそういう位置づけになるのかもしれません

ソースはダウンロード済みですが自分で打ち込みながら進めようと思います
全ソースコードが載ってるかどうかは微妙に不安

読者のみなさんも、できれば好きな言語でJ-Bobとその言語を実装してみてください。

J-Bobの組み込み関数さえ互換性のある形で実装できればあとは同じコードでいけるはずだしね
Racketで書いてみようかなと思いましたがRacketでは組み込み関数の上書きが許されていないので
単純な形では実装できなさそうでここはあきらめておきます
RacketでACL2が書いてあるほどなのでできないわけではないはずですがちょっと大掛かりに
なるんじゃないかと
Readerをいじったりとか

ごく単純な言語なので、Scheme修行のインタプリタを手直しして使うとかすると面白いかもしれませんね？
Scheme手習いのインタプリタはdefineすらないのでさすがに不足なのが明らか

というわけなので

SchemeでJ-Bobを使うには

ACL2の方ではなくてこっちでいきます