きゅーけー @tojoqk@mastodon.tojo.tokyo

ACL2 でブラックジャックの勝敗判定を実装してみた。
Lisp だけど全ての関数が停止することを証明しているし、重要な関数の戻り値が期待したものになることも証明している。静的型付けとは異なる証明への道へ歩み始めた。

https://gitlab.com/tojoqk/blackjack/

Guile で動く定理証明支援系を作った。だいたい自分の望むものは手に入ったので、とりあえずはこれを使って『定理証明手習い』を一周してみようと思う。

https://gitlab.com/tojoqk/vikalpa

開発者による支配から身を守るために自由ソフトウェアを使いましょう
https://www.tojo.tokyo/freedom-for-yourself.html

寝よう……

シャワーを浴びているときに、ace のスコア計算で無駄に再帰しているせいで証明が大変になっていることに気づいた。
https://gitlab.com/tojoqk/blackjack/-/commit/4bf52294c02c89c5cbd44689fcf573bb29cf1204

https://mastodon.tojo.tokyo/@tojoqk/105606459763642932

ACL2 で書いたブラックジャック、任意の枚数のカードで、score が 11 以下のときにもう一回カードを引いても BUST しない定理の証明に成功したのでだいたい満足した。 https://gitlab.com/tojoqk/blackjack/-/commit/60143c0e574d00a1571bd0750ca7186cdc4d04dc

歯医者終わった。ハイブリッドセラミックの歯が取れたので付けてもらった。保証期間内だったらしく無料で交換してもらえたので良かった。

外寒そうだけど予約済みの歯医者に行く

これが人生で初めて乗った救急車なんだけどなんも覚えてない。救急車の中ではサイレンの逆位相の音を出してサイレンの音を打ち消しているため静かだという話を聞いたことがあるので機会があれば確かったけど無理だった。

それまでは日常的にお酒を飲んでたので、ある意味この出来事に助けられた。

目覚めたとき若干残念そうにしていた看護師のことを未だに覚えている。たぶん、何か準備をしていたんだと思うので申し訳ない。

しかもこのとき30分起きるのが遅かった場合は起こす処置をするために10万円請求されるところだったらしい。それ以来はお酒を飲むのはやめた。コーラゼロとかでいい。

酔いが分からないは言い過ぎで、やばくなっても自覚できないという感じ。病院に運ばれたときは記憶が完全に消えててもう対策の仕方が分からなかった。

アルコール、酔いを自覚できなくて一度病院に運ばれたことがあり、それ以来一切飲まなくなった。百害あって一利なし。

歯医者行くの怠すぎるな

総当たりで解決しちゃっている感はある

expand のヒントの使い方を覚えたことで、11 以下のときは安全にヒットできることを示す定理がかけた。

https://gitlab.com/tojoqk/blackjack/-/commit/12733bfa51f3cc6c98d2b067bf3217f4e2a76145

このチュートリアルめっちゃ重要だった。thm と verify コマンドと expand ヒントの使い方を覚えたぞ。
https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#top

#ACL2

あれ、昨日ヒントを書かないと証明してくれなかったやつが今日は書かなくても普通に証明してくれるのなんで？深夜の謎のテンションで書いてたのが悪かったのかな……。

#ACL2

仕事終わった後寝てた。今週も疲れた。

lambda のない Lisp を Lisp と呼んでいいのか謎

とりあえず 16 の以下のときには hit してもバーストしない定理を書きたい。