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

10375 ワード
Scheme prover lisp Scheme テキストリンク

はじめに

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

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

おわりに

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

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

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

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