J-Bob に会いにジャンピング土下寝

環境構築ってなんでこんなに大変なんだろうね。

結論

ちょっと古い DrRacket 7 系を使うことで、Scheme 版も ACL2 版？もとりあえず動いてるような気持ちにはなれた。

参考

動機

定理を証明していきたくなってきた。Coq はなんだか大変そうだ。
そんな我々に the-little-prover。
和書もあるよ (さすがラムダノート！俺たちに出来ないことを平然とやってのける。ありがとうございます。)
http://the-little-prover.github.io/
https://www.lambdanote.com/collections/littleprover

状況

右も左もわかっていない。

とりあえず J-Bob を探してあちこち尋ねたところ、 Racket 8 系で Dracula を入れようとしても無理ということはわかった。

dracula、どうしてしまったんや

Racket 8 系で Dracula を入れようとすると何となく入りそうなそぶりを見せるのだが、どうもふがふが言ってうまく入らない。

Racket 7 系まではとりあえず動いていたようで、8 系で出力されているエラーをチラ見した感じでは、そこはかとなく

この辺 (vv7.9 ってなんだ？) と
https://github.com/racket/htdp/releases/tag/vv7.9
https://github.com/racket/htdp/releases/tag/v7.9

この辺で、
https://github.com/racket/htdp/releases/tag/v8.0

生じたパスの構成変更に dracula が追従できていなさそうな気がした。
他にも問題があるのかないのかは不明。

というイシューで言及されているのと同様のログが手元の Racket 8.4 (Windows 環境) でも見受けられた。

実際、
https://github.com/racket/htdp/blob/vv7.9/htdp-lib/test-engine/scheme-gui.rkt

というファイルは htdp 7 系にはあったようだが、

にはそういうのは見つからない。

これがどういう状況なのかわからないが、とりあえず面倒だから Racket 7.9 を入れたら何事もなかったかのように環境は構築できた。できた？
ような気がするのでとりあえずよし。

Racket 使うなら

これでいいんじゃね？的な PR も観測されたが詳細不明。

で、どうなってるか

結局 scheme ベースの方でちょこちょこ見ている (Dracula とは何だったのか、、、)。

chapter1.scm

;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")
;; Load the transcript of all proofs in the book:
(load "little-prover.scm")

(J-Bob/step (prelude)
  '(car (cons 'ham '(eggs)))
  '())


(J-Bob/step (prelude)
  '(car (cons 'ham '(eggs)))
  '((() (car/cons 'ham '(eggs)))))

(chapter1.example1)

output

(car (cons 'ham '(eggs)))
'ham
'ham

' は？

' が一個ずつ少ないような気がしてるのだけど、どうも Racket 的には暗黙の quotation があったりなかったり？

Many forms are implicitly quoted (via #%datum) as literals.

この理解が正しいか自信ないが、出力の設定をいじると quote の存在がうっすらうかがえた (そういう話ではないかもしれないが)。

• Output Style: Constructor

• Output Style: write (これだと、ぬるっと ' が一つ足りないように見える。気がする)

• Output Style: print

Racket の話ではなく、R5RS の仕様の話とかなのかな？？

4.1.2 Literal expressions
scheme
syntax: (quote <datum>)
syntax: '<datum>
syntax: <constant>

(quote <datum>) evaluates to <datum>. <Datum> may be any external
representation of a Scheme object (see section 3.3). This notation is used
to include literal constants in Scheme code.

(quote a)                             ===>  a
(quote #(a b c))             ===>  #(a b c)
(quote (+ 1 2))                       ===>  (+ 1 2)

(quote <datum>) may be abbreviated as '<datum>. The two notations are
equivalent in all respects.

'a                           ===>  a
'#(a b c)                   ===>  #(a b c)
'()                          ===>  ()
'(+ 1 2)                     ===>  (+ 1 2)
'(quote a)                   ===>  (quote a)
''a                          ===>  (quote a)

Numerical constants, string constants, character constants, and boolean
constants evaluate ``to themselves''; they need not be quoted.

'"abc"             ===>  "abc"
"abc"              ===>  "abc"
'145932            ===>  145932
145932             ===>  145932
'#t          ===>  #t
#t           ===>  #t

As noted in section 3.4, it is an error to alter a constant (i.e. the
value of a literal expression) using a mutation procedure like set-car! or string-set!.

(quote datum)

Produces a constant value corresponding to datum (i.e., the representation of the program fragment) without its lexical information, source location, etc. Quoted pairs, vectors, and boxes are immutable.

わかんねー。

おまけ

proof pad というのでブラウザで ACL2 をお試しできるらしい。でも http。
http://new.proofpad.org/