ACL2 でブラックジャックの勝敗判定を実装してみた。
Lisp だけど全ての関数が停止することを証明しているし、重要な関数の戻り値が期待したものになることも証明している。静的型付けとは異なる証明への道へ歩み始めた。
Guile で動く定理証明支援系を作った。だいたい自分の望むものは手に入ったので、とりあえずはこれを使って『定理証明手習い』を一周してみようと思う。
開発者による支配から身を守るために自由ソフトウェアを使いましょう
https://www.tojo.tokyo/freedom-for-yourself.html
シャワーを浴びているときに、ace のスコア計算で無駄に再帰しているせいで証明が大変になっていることに気づいた。
https://gitlab.com/tojoqk/blackjack/-/commit/4bf52294c02c89c5cbd44689fcf573bb29cf1204
ACL2 で書いたブラックジャック、任意の枚数のカードで、score が 11 以下のときにもう一回カードを引いても BUST しない定理の証明に成功したのでだいたい満足した。 https://gitlab.com/tojoqk/blackjack/-/commit/60143c0e574d00a1571bd0750ca7186cdc4d04dc
これが人生で初めて乗った救急車なんだけどなんも覚えてない。救急車の中ではサイレンの逆位相の音を出してサイレンの音を打ち消しているため静かだという話を聞いたことがあるので機会があれば確かったけど無理だった。
expand のヒントの使い方を覚えたことで、11 以下のときは安全にヒットできることを示す定理がかけた。
https://gitlab.com/tojoqk/blackjack/-/commit/12733bfa51f3cc6c98d2b067bf3217f4e2a76145
このチュートリアルめっちゃ重要だった。thm と verify コマンドと expand ヒントの使い方を覚えたぞ。
https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#top
あれ、昨日ヒントを書かないと証明してくれなかったやつが今日は書かなくても普通に証明してくれるのなんで?深夜の謎のテンションで書いてたのが悪かったのかな……。
GNU Guix ユーザーの Schemer で、自由ソフトウェアと行動分析学が好きです。
通状況的一貫性が保証されない性格を調べるための性格テストに反対します。
好きなソフトウェア
OS: GNU Guix
プログラミング言語: GNU Guile (Scheme)
エディタ: GNU Emacs
Window Manager: EXWM (Emacs)
クラウドサービス: Nextcloud