ACL2 でもやった(ただ計算によって比較しただけなので、この定理証明に ACL2 のうまみはない)。
これを一般化したようなものを証明できたら凄そうだけど大変そうなのでやらない。
あ、coalton 側で tail recursion の最適化はしてくれないっぽいな。普通に SB-KERNEL::CONTROL-STACK-EXHAUSTED って言われてしまった。下の関数に (neko 100000) って入れただけなのに。これは回避法の模索が要るな。
Coalton が関数型言語である以上、処理系に依存してでも末尾再帰は最適化されて欲しいところがある。
忙しい人はまあこれだけ見ればなんで山本一太群馬県知事が「魅力度ランキング」なるものに対してあんだけ攻撃的な態度(なお、本人としては冷静であり攻撃的な態度をしているとは認識していない様子)をとっているのか分かるだろう。
既に7月の時点で群馬県庁サイドによる「魅力度ランキング」に対する分析を終えていて、ブランド総合研究所は「魅力度ランキング」という名称に相応しい調査ができているとはいえず、杜撰なランキングであるという結論を出した上で、再度ブランド総合研究所が魅力度ランキングを発表し、メディアがそれを取り上げて社会的な影響を与えたという文脈があるわけだ。
いきなり山本一太知事が怒りくるったわけではないことがよく分かる。
いけたわ……。Emacs がダイナミックスコープであることを利用して let で org-capture-templates を束縛してから org-capture を呼び出す関数を定義すれば文脈に応じて別の org-capture を呼びだせる。
これで org-capture の可能性が爆発的に広がった。TODO で t が既に取られているから体温は T にするかーとかもう考えなくていいんだ……。
さっきの頼まれごとの正体は文字列のリストから n 個を取りだす全ての組合せを求めて欲しいというものだったんだけど、ACL2 で実装した。とりあえず組合せの数に関する定理を書いたら補助定理なしで自動証明できてしまって驚いた。
コード: https://git.tojo.tokyo/acl2-theorems.git/tree/combinations.lisp?id=975418f4c2e1520649196458d3211e6ef9ec531a
ACL2 の出力: https://ci.tojo.tokyo/jobs/acl2-verify/412
GNU Guix ユーザーの Schemer で、自由ソフトウェアと行動分析学が好きです。
Jami: e5fdfccb74c383420e6e647897dae018a4bd61fb