Pinned toot

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

gitlab.com/tojoqk/blackjack/

Pinned toot

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

gitlab.com/tojoqk/vikalpa

Pinned toot

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

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

Show thread

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

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

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

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

Show thread

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

Show thread

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

Show thread

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

Show thread

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

Show thread

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

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

gitlab.com/tojoqk/blackjack/-/

Show thread

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

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

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

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

Show thread

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

Show more
Mastodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!