Show newer

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

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

Show thread

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

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

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

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

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

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

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

再帰よりループの方が表現力が低いのでループの方を積極的に使う

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

再帰よりもループの方が実行順をソースコードの字面で追いやすいかも。再帰を追うには頭の中にスタックを置く必要がある。

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

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

Show thread

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

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

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

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

ACL2 - Logical-story-of-io
cs.utexas.edu/users/moore/acl2

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

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

Show older
Mastodon

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