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

プログラムとデータの境界は曖昧であり、S式でかかれたデータがプログラムなのかそれともデータなのかを明確に区別することはできない。人がそれをデータと呼ぶかプログラムと呼ぶかの差でしかない。S式で記述された設定を解釈するプログラムを書いているときそれを強く感じる。そのプログラムは設定ファイルのインタープリタであり、設定ファイル側がプログラムだと見てもなんらおかしくない。Lisp だと扱うデータとプログラムの形が似てるのでそういう気持ちに入りやすい。

だって、S 式でかかれていれば `read` 関数で読めるんだもん。構文解析する手間が省けてよい。こんなに楽な話があるだろうか。

Lisp 界隈では構成ファイルを S 式で書くのがどう考えても最も合理的なんでむしろ他の方法で設定している方が不思議なレベルに見える。

順序数の尺度で停止性を証明できる関数は実はだいぶ限られてるんかな。停止しそうなのに停止性が証明できてないやつコラッツの関数くらいしか知らないや。

ともかく何かが再帰するたびに減りさえすればいい。そうすれば必ず停止する。そういう風に作ればいい。

「わるあがき」だった。

ポケモンの戦闘のシステム(ppが尽きると「がむしゃら」という自分のHPを削るわざしか使えなくなる)を参考にすればターン制の戦闘ゲームの停止性が保証できるということにこの前気づいたんで、ACL2 でそういう感じの戦闘ゲーム作ろうかな。再帰する度に何らかの順序数の尺度が減るように設計すれば確実に停止することを示せる。

そんな簡単じゃないなこれ。あとで思いだしたときに再チャレンジしよう。

これ arithmetic ライブラリに加えて補助定理を一個書くだけで証明できるかもという期待と、自分の考えている補助定理の証明にどれくらい時間がかかるかという不安がせめぎあっている。解けたらせっかくなので記事にしようかな。

あれ？ちゃんと全部大文字だった。どこで ACL2 が Acl2 に変わったんだろう。

というか、なんでタイトル ACL2 じゃなくて Acl2 になってるんだろう。即座に直そう……。

う、ACL2 の arithmetic ライブラリをロードしようと思って調べたら雑な自分の記事がでてきてつらい……。Japan を有効にしてなければ出てこないだけ幸いである。

これ> 証明に成功しました。定理ライブラリの力は凄いですね。とか書いてあるやつなので検索されて見つけられるの恥かしいんだよな。

一般解を ACL2 で求めるのいけるかもしれないのでちょっとやってみるか。あんまり時間かかりそうなら諦めよう。

この人 x^x 乗が好きでたまらない人なんかな。

動画をちゃんとみていけそうならやるか。

ACL2 でもやった(ただ計算によって比較しただけなので、この定理証明に ACL2 のうまみはない)。これを一般化したようなものを証明できたら凄そうだけど大変そうなのでやらない。

ACL2 用の Emacs の設定と Common Lisp を普通に使うようの設定が競合を起こさないか気にしてたんだけど意外と矛盾しないかも。

こんな感じでちゃっちゃっと求められてしまう(動画のネタバレ回避のため閲覧注意)。

Guile には 「こうかつ、ずるさ、悪知恵」という意味があるんでしゃあない(関係ない)。https://ejje.weblio.jp/content/guile

これはいまどきの計算機なら、多倍長整数を使って簡単に求められてしまうな。Guile を使ってぱぱっと比較してしまった(数学しろ)。https://www.youtube.com/watch?v=BNa8eJqjB6I