「定理証明手習い(The Little Prover)」のJ-Bobを動作させる Scheme版/ACL2版

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/36113a2a-2843-16c1-eb23-13c1f81a2f89.png)

# はじめに

「xxx手習い」(原書:The Little xxx-er)というシリーズをご存じでしょうか。
これらの本はどれも、「会話式」という独特の形式で内容が進行する、面白い本です。
基本的に手書き確認で読み進められる本だだと思っているので、読み進めるにあたって、実際の処理系は必要ないかもしれませんが、処理系を使う事で、より確信が持って読み進められる、という場合もあるかと思います。

さて、Lambda Noteから訳本として出版されている「定理証明手習い(原書：The Little Prover)」ですが、途中から「J-Bob」というライブラリを利用している形になっています。

内容解説みたいはのもやりたい気はしますが、まだ勉強中なので、とりあえず、J-Bobの動作環境を設定するところまで、共有しておきます。

# まず、ググる

「little prover j-bob」で検索すると、先頭に

[the-little-prover/j-bob - GitHub](https://github.com/the-little-prover/j-bob)

が引っ掛かります。まさにここですね。そして、このリポジトリの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版がある、とあります。確かに、リポジトリの階層を見ると、以下の様にになっています：

```sh

└─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](https://racket-lang.org/)の[Dracula](https://pkgs.racket-lang.org/package/dracula)パッケージに含まれる、みたいな事が書いてあります。自分はRacketもDraculaも知りませんでしたが、動作環境を作るにはまずはこれかなと思い、インストールしてみます。

# Racketのインストール

https://racket-lang.org/

に行って、右上のダウンロードボタンを押して、各動作環境に合わせたものをダウンロードします。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/7ce150f6-2767-2edb-72be-8873928e4152.png)

自分は、これで：
![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/5fd5dcdc-1e15-8d4e-8312-80fec62c0b7a.png)

ダウンロードしてインストーラでインストールすると、スタートメニューから起動できるようになります。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/dfc466c2-30ee-5b7c-a265-3080b4162067.png)

起動時のスプラッシュ（特にここに張り付ける意味なし・・）

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/ad095e23-2b62-2ba8-b199-3df84ce6c0b3.png)

# Racketの起動画面
![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/63111068-b6f0-369e-1b9c-abb3cd93b3ec.png)

# REPLを使ってみる

エディタとREPLの統合環境が起動します。Scheme処理系との事なので、ひとまず、REPL側でいくつか式を評価してみました。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/14714b95-db02-7882-eb21-f858aee4c5ad.png)

# エディタを使ってみる

エディタに式を入力して、右上のRunボタンを押して評価をしました。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/1ff813af-a46f-56aa-7eb2-68c0e5337394.png)

普通のScheme処理系です。これを使ってThe Little SchemerやThe Little Proverを確認しながら読むのが良いかもしれませんね。

# Scheme版を試す

## Language設定

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/587c08c4-f1bf-c1c1-f24f-d30a57c3504d.png)

Languageメニュー/Choose Languageで、言語の選択画面を開きます。ここで、以下の設定を行います。

- Other Langueges / R5RS
- Initial Bindings / Disallow redefinition

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/89538267-ac6d-da2a-0b4e-5262b25e75f6.png)

## GitHubからクローンしたRepositoryフォルダschemeにファイルを作り、開く

適当なファイルjbobwork.scmなど）を作って、リポジトリフォルダをschemeフォルダの下に置き、
それを、Racketのファイルメニューから開きます。
この作業をどうしてやったかといえば、J-Bobの定義ファイルが置いてある、schemeフォルダをRacketの作業ディレクトりにしたかったからです。他にやり方はわかりませんでした。

開いた、ファイルに、以下を書き込み、Runで実行してみます。

```scheme
(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)))))
```


## 結果

以下の様に結果がでます：

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/f177223f-d163-f3e7-a91d-4ab04713b682.png)

一応、本通りの結果になっているようですね。

# ACL2版を試す

LanguageSettingでACL2/Draculaは選べませんでした。これは、Racketのパッケージとして追加でインストールする必要がありそうです。メインメニューから、　PackageManagerを起動します。

そして、Package Sourceというテキストボックスに「dracula」と入れてエンターキーを押したら、パッケージのダウンロードやインストールが始まってしまいました。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/bfa3c6fa-44f5-fc6e-1353-777d5bc22b97.png)

実際にはracoというパッケージマネージャが動作しているようです。

## Language設定
Draculaインストール後に、再度Language設定を開くと、Dracula/ACL2が選べるようになっているので、選びます。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/8e8983b5-45c6-89c8-f07a-156186d303d1.png)

## GitHubからクローンしたRepositoryフォルダacl2にファイルを作り、開く

schemeの時と同様に、適当なファイルjbobwork.lispなど）を作って、リポジトリフォルダをacl2フォルダの下に置き、それを、Racketのファイルメニューから開きます。
ファイルには、以下の内容を書き込み、Runボタンで起動します。

```lisp
(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の場合と同様、以下の様に結果がでます。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/101445/b92e3816-ea1f-d9df-7c03-c12a29c41af6.png)

こちらも、結果は問題無いようですね。

# おわりに

今回のメモは、以下の２つのブログを参考にさせていただきました：

- https://lorinstechblog.wordpress.com/2017/10/22/j-bob-from-the-little-prover/
- http://kb84tkhr.hatenablog.com/entry/2018/01/01/161525

特に技術的に深い解説などでなくても、こういうちょっとした「メモ」が自分の作業に助けになる、というのを再確認しました。

また、この作業の中で、DrRacketという処理系をはじめてつかってみました。今後、こちらも使ってみたいと思います。

以上、「定理証明手習い」を独学している人たちの参考になれば。