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

再帰関数を読むときに最初から計算の途中経過について考えるのをやめてもらう必要がある気がする。関数について理解してから途中経過について考えるのは難しくないはずでこの読み方をすればループより簡単だと思うようになるはず。

私の場合は脳内メモリが貧弱なので再帰関数の方が簡単でいいんだけど、脳内メモリが潤沢にある一般的な人々には手続き型な方が扱いやすいみたいなことがあるのかもしれない。

ツイッタで一般に再帰はループよりも難しいとしてる話があって、逆かと思ったんだけど逆じゃなかった。ACL2 を普及させたいなーと思ってたけど、多くのプログラマにとってそれ以前に巨大な壁が立ちはだかっていることに気付かされた。

Guix に vim-slime なるパッケージが追加されたのを観測した。https://ci.tojo.tokyo/jobs/guix-update/24

私の CI サーバーのマシンパワーが低すぎて ACL2 とよく使われるライブラリのビルドが 2 時間経過しても終わらない。https://ci.tojo.tokyo/jobs/guix-update/19

過去に ACL2 では副作用を扱う場合は :program モードにすればいいのかとか言ってたけど、間違ってた。ACL2 はファイル入出力などの副作用を扱う処理についても扱えて定理証明できることを知った。どうやっているのかのロジックは論文を読まないと無理そうで今はその体力はないのでそこまで調べるのは諦める。

ACL2 - Logical-story-of-iohttps://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____LOGICAL-STORY-OF-IO

ACL2 のユーザーマニュアルを毎回探し回るの間抜けなのでブックマークした。

諸事情であんまり頭を使えなくなっているので、ACL2 で軽く入出力をする方法だけ調べるだけにしよう。

8/5 に ACL2 の最新のバージョンが 8.3 から 8.4 に上がってた。全く気づかなかった。。。https://www.cs.utexas.edu/users/moore/acl2/

Jupyter Notebook で書いたのを Guile の haunt のブログ記事にする仕組みがうまく動いていて快適だ。

s/重要/需要/

重要があるのか謎だけど ACL2 に関する記事を書いた。この記事を読んでも ACL2 が使えるようになる要素は皆無なんだけど、ACL2 でどんなことができるかは日本語で発信していくべきだと思うのでしばらく続けようと思う。https://www.tojo.tokyo/comb-factorial.html

ACL2 で組み合わせの数の階乗表現について証明しことの記事を書いてたんだけど、読者から見て分かるように補助定理を書いた理由が説明できない……。なんとなく書いておいた定理が良い感じに発火して証明できたので……。

組み合わせって、組み合せじゃなくて組み合わせという方が一般的なのか。全部組み合せって書いてた……。SKK の設定を見直した方がよさそう。

1=2 ならば全ての猫は爬虫類に属する(古典論理では真)

ACL2 が式変形した結果、仮定が偽になっているやつが見つかり、全体を真にするために仮定が偽であることを証明するということがたまによくある。

ACL2 を使ってると古典論理に支配されてしまう感じがする。特に p -> q で p が偽のとき真という異常な感覚が養われつつある。

日本は「いろはにほへと」のイメージを勝手に持ってた。あいうえお順っていつからあるんだろ。

ここの部分最高だな。センス抜群なのでは。

> "We all deserve control over our digital lives. [..] It's time to stand up for the right to privacy -- yours, mine, all of ours. This problem is solvable -- it isn't too big, too challenging, or too late.">> Thanks, Tim Cook. We couldn't agree more, and we hope you'll tell Tim you agree with him on this one, too.

実際、OpenVPN のサーバーは過去に数回建てたことがあるのに苦戦した。でも Guix を使ったからきっとこれは最後の苦戦なのだ。