はじめに
「xxx手習い」(原書:The Little xxx-er)というシリーズをご存じでしょうか。
これらの本はどれも、「会話式」という独特の形式で内容が進行する、面白い本です。
基本的に手書き確認で読み進められる本だだと思っているので、読み進めるにあたって、実際の処理系は必要ないかもしれませんが、処理系を使う事で、より確信が持って読み進められる、という場合もあるかと思います。
さて、Lambda Noteから訳本として出版されている「定理証明手習い(原書：The Little Prover)」ですが、途中から「J-Bob」というライブラリを利用している形になっています。
内容解説みたいはのもやりたい気はしますが、まだ勉強中なので、とりあえず、J-Bobの動作環境を設定するところまで、共有しておきます。
まず、ググる
「little prover j-bob」で検索すると、先頭に
the-little-prover/j-bob - GitHub
が引っ掛かります。まさにここですね。そして、このリポジトリのREADME.mdには、以下の様に書いてあります
This repository contains "J-Bob", the proof assistant from "The Little Prover"
by Daniel P. Friedman and Carl Eastlund, published by MIT Press in 2015.
We include the necessary code to run J-Bob in ACL2 and Scheme, as well as a
transcript of the proofs in the book. J-Bob is also included in the Dracula package
for Racket.
ALC2判とScheme版
J-Bobは、ACL2判とScheme版がある、とあります。確かに、リポジトリの階層を見ると、以下の様にになっています：
└─j-bob
│ .gitignore
│ LICENSE.md
│ README.md
│
├─acl2
│ j-bob-lang.lisp
│ j-bob.lisp
│ little-prover.lisp
│
└─scheme
j-bob-lang.scm
j-bob.scm
little-prover.scm
Dracula/Racket ??
RacketのDraculaパッケージに含まれる、みたいな事が書いてあります。自分はRacketもDraculaも知りませんでしたが、動作環境を作るにはまずはこれかなと思い、インストールしてみます。
Racketのインストール
に行って、右上のダウンロードボタンを押して、各動作環境に合わせたものをダウンロードします。
自分は、これで：
ダウンロードしてインストーラでインストールすると、スタートメニューから起動できるようになります。
起動時のスプラッシュ（特にここに張り付ける意味なし・・）
Racketの起動画面
REPLを使ってみる
エディタとREPLの統合環境が起動します。Scheme処理系との事なので、ひとまず、REPL側でいくつか式を評価してみました。
エディタを使ってみる
エディタに式を入力して、右上のRunボタンを押して評価をしました。
普通のScheme処理系です。これを使ってThe Little SchemerやThe Little Proverを確認しながら読むのが良いかもしれませんね。
Scheme版を試す
Language設定
Languageメニュー/Choose Languageで、言語の選択画面を開きます。ここで、以下の設定を行います。
- Other Langueges / R5RS
- Initial Bindings / Disallow redefinition
GitHubからクローンしたRepositoryフォルダschemeにファイルを作り、開く
適当なファイルjbobwork.scmなど）を作って、リポジトリフォルダをschemeフォルダの下に置き、
それを、Racketのファイルメニューから開きます。
この作業をどうしてやったかといえば、J-Bobの定義ファイルが置いてある、schemeフォルダをRacketの作業ディレクトりにしたかったからです。他にやり方はわかりませんでした。
開いた、ファイルに、以下を書き込み、Runで実行してみます。
(load "j-bob-lang.scm")
(load "j-bob.scm")
; p153[3]
(J-Bob/step (prelude)
'(car (cons 'ham (eggs)))
'())
; p154[7]
(J-Bob/step (prelude)
'(car (cons 'ham '(eggs)))
'((() (car/cons 'ham '(eggs)))))
結果
以下の様に結果がでます：
一応、本通りの結果になっているようですね。
ACL2版を試す
LanguageSettingでACL2/Draculaは選べませんでした。これは、Racketのパッケージとして追加でインストールする必要がありそうです。メインメニューから、 PackageManagerを起動します。
そして、Package Sourceというテキストボックスに「dracula」と入れてエンターキーを押したら、パッケージのダウンロードやインストールが始まってしまいました。
実際にはracoというパッケージマネージャが動作しているようです。
Language設定
Draculaインストール後に、再度Language設定を開くと、Dracula/ACL2が選べるようになっているので、選びます。
GitHubからクローンしたRepositoryフォルダacl2にファイルを作り、開く
schemeの時と同様に、適当なファイルjbobwork.lispなど）を作って、リポジトリフォルダをacl2フォルダの下に置き、それを、Racketのファイルメニューから開きます。
ファイルには、以下の内容を書き込み、Runボタンで起動します。
(include-book "j-bob-lang" :dir :teachpacks)
(include-book "j-bob" :dir :teachpacks)
; p153[3]
(J-Bob/step (prelude)
'(car (cons 'ham (eggs)))
'())
; p154[7]
(J-Bob/step (prelude)
'(car (cons 'ham '(eggs)))
'((() (car/cons 'ham '(eggs)))))
結果
Schemeの場合と同様、以下の様に結果がでます。
こちらも、結果は問題無いようですね。
おわりに
今回のメモは、以下の２つのブログを参考にさせていただきました：
- https://lorinstechblog.wordpress.com/2017/10/22/j-bob-from-the-little-prover/
- http://kb84tkhr.hatenablog.com/entry/2018/01/01/161525
特に技術的に深い解説などでなくても、こういうちょっとした「メモ」が自分の作業に助けになる、というのを再確認しました。
また、この作業の中で、DrRacketという処理系をはじめてつかってみました。今後、こちらも使ってみたいと思います。
以上、「定理証明手習い」を独学している人たちの参考になれば。