Notices by きゅーけー (tojoqk@mastodon.tojo.tokyo), page 255

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

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

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

Common Lisp では foo->bar は foo-to-bar と書く空気があるんだろうか。

CLiki: Naming conventions https://www.cliki.net/Naming+conventions

なぜ、atom と null は atomp と nullp ではないのか…

昔 C 言語の課題で述語の関数の名前の末尾に p を付けたやつを提出しちゃったことある気がする。あれは意味不明だろうな……。

ACL2 を使いはじめて、 ? を p と書くのに慣れてきている自分が恐しい。なんとなく ? よりも p の方が良い気さえしてくる(Lisp の述語の命名規則の話です)

Racket だと natural? は exact-nonnegative-integer? の別名として定義されてる。

4.3.2 Generic Numerics https://docs.racket-lang.org/reference/generic-numbers.html?q=natural%3F#%28def._%28%28lib._racket%2Fmath..rkt%29._natural~3f%29%29

今のところ自然数で停止性を証明できない関数にであってない。

TL で整数と無限の話があがってて ACL2 を学ぶ過程で順序数の勉強をしないといけないことを思い出した。

Common Lisp で p (predicate の p) を付けるときの命名規則。

6. Predicateshttps://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node69.html

#qk_note

Scheme 派なんだけど、 ACL2 を使うために Common Lisper になるしかないな。

vikalpa はこれhttps://mastodon.tojo.tokyo/@tojoqk/105579715190206801

ACL2 でうまくルールを作ることで自動証明がうまく動く様を見ると手動で証明する気が失せるな。さっそく vikalpa の開発モチベが地に落ちた気がする。

ACL2 の全ての関数が全域であり、引数の制約は guard でできるという考え方。最初はそれに納得がいかなくて別の道がないか模索したけど結局 ACL2 の選択が優れていると実感するだけだったな。

餅はリスクに対して得られる益が低過ぎるので避けてる。

ソースコードではなく emacs の設定ファイルとして捉えれば、EDIT THIS SECTION って書いてあるのは当然か。

ソースコードに EDIT THIS SECTION って書いてあるの初めてみたかもhttps://github.com/acl2/acl2/blob/master/emacs/emacs-acl2.el#L157-L172

いずれにしても guix.scm は書くけど

ACL2 を使いたいのにまずは Guix のパッケージングをしようとか言い出すのは本末転倒っぽいのでまずは手元で動かして便利に使うところから始めよう。

https://guix.gnu.org/en/packages/acl-2.2.53/すでに acl の version 2 というほぼほぼ同じ名前っぽい別のソフトウェアがあるの草。ここに ACL2 が追加されるのカオスでは。