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

Mastodon に CI の通知をする設定はこれ。https://git.tojo.tokyo/ci.git/tree/after?id=c7a1cfeb5b7e28b26fa73ae1c27fa517040abe04

Laimnar CI は自由度が高くて本当によい。Laminar CI をベタ褒めしている記事はこれ。https://www.tojo.tokyo/laminar-is-best.html

CI からの通知を Mastodon で受け取れるようにした。https://mastodon.tojo.tokyo/@ci/106928168549286055

toot のテスト

@tacumi 流石にメモリを多く使用しているやつから kill してくれないと役に立たないので完全にランダムということはないと思ってました。調べてみると /proc/<pid>/oom_score なるファイルを確認することで OOM のスコアがわかるみたいで、/proc/<pid>/oom_score_adj を編集することで OOM による kill されやすさを調節できるらしいです。

たしかに、何度か経験ある。メモリ4GBのラップトップのメモリを食い尽くして反応しなくなってなんどか強制終了した記憶ある。なぜ速やかに OOM で殺されてくれないんだろうか。

s/現実都鄙/現実逃避/

なんだこの誤字、どうやったんだ……。

現実都鄙パワーによって記事の作成が捗りまくっている気がする。ぽんぽん記事を書いていこう。

Guile ではスタック溢れを気にせずに再帰して良い件について記事を書いた。https://www.tojo.tokyo/guile-recursion.html

自分をなんでも Emacs でやる系の人だと勝手に思っていたが、Jupyter Notebook を導入してからはそればかりを使うようになった。どうやら私は org-mode よりも Jupyter Notebook の方が性に合うようだ。

Book マネージャか

Guix を ACL2 のパッケージマネージャにできる気がしてきた。

Guile で書いたプログラムを紹介する記事を書いた。https://www.tojo.tokyo/guile-df.html

Jupyter Notebook が想像以上にいい。Jupyter Notebook で Guile と ACL2 が動かせるようになったのでもう十分な感じする。

Guile とか Racket みたいに非末尾再帰な関数でスタックオーバーフローを起こさない Common Lisp 処理系がないか気になってる。

Guile とか Racket だと末尾再帰にしなくてもスタックオーバーフローは起こさないので他のプログラミング言語やってる人と感覚がずれている可能性もある。そもそも私の書くプログラムで本当に末尾再帰にしないとまずいやつって稀だし。。。(そんな巨大な数やデータを扱うことがない)

ACL2 は Common Lisp のサブセットだから本当に LISP だよ！って言いたいけど lambda 式を失った LISP のことを人々が LISP として認めてくれるのかどうかが怪しい。cons セルがあってコードがリストでマクロが使えるところまでは LISP らしさある。

ちゃんと寝むくなってきた気がする。いまこそ寝るときだ。

普通の再帰関数の方が帰納法で性質を示しやすいので出番がある。効率を気にする場合は末尾再帰版との等価性を証明できればよい。

ただ、末尾再帰関数の性質について直接証明をする方法もそれはそれで重要なため両方のスタイルで証明ができた方がよいと下記の練習問題の回答にあった(ものによっては末尾再帰でないバージョンと等しいことを示すのが難しい場合もある)。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____INTRODUCTORY-CHALLENGE-PROBLEM-4

まあ、ともかく ACL2 なら末尾再帰版でない関数にも出番があるのだ。

定理証明をするときには末尾再帰してない普通の再帰関数に価値があるのでよい。それ以外の文脈だと大抵の場合は末尾再帰版やループの方がよいという結論になるのは分かる。

末尾再帰関数で状態を回すやつはループと見做して考えていた。再帰とループの話、雑に話すと色んな話が混みあってしまう感じある。