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

スキナーが弱化のことを罰って命名していたのにはそれなりの思想的な背景がおそらくある。それをいうと負の強化は専門用語的に罰ではないが実際には罰的と言わざるを得ないわけで、そう考えると好子と嫌子という用語はスキナーの思想をよりうまく汲み取った優れた用語ということができる気がする。

好子と嫌子を使うと負の強化は「嫌子消失による強化」となりなんか強化だけど悪いイメージになり、そういうイメージが付くこと自体は専門用語的に正確でないが、思想的に悪いことではないようにみえる。

「負の強化」と「正の弱化」と「負の弱化」あたりがたぶん理解に失敗するポイントだと思う。行動随伴性のうち 3/4 が理解に失敗しうるとか致命的なのでは……。

行動分析学の強化と強化子まわりの用語が分かりにくすぎる問題やっぱあるな。やっぱ好子と 嫌子でよかったのでは……。

ACL2 の本、どういう保存のされかたしてたんだか謎なんだけどなんか臭うんだよな。本に染み付いた臭いを消す方法を知りたい。

コンビニによって帰ってきたら、冷静に考えてみたら別に数学をすることではなくてプログラムの性質を証明したいのであって順序数についてある程度分かったなら ACL2 をやったらよくね？って気が変わって ACL2 モチベが上がってきた。これぞ諸行無常……。

無限集合に飽きたら ACL2 に戻ろう。

ACL2 を使っていきたかったが、無限の誘惑には勝てなかった……。

なんか Coq で集合論できそうな気配がするので Coq と Proof General のインストールを始めた。

Isabelle は ZFC をサポートしてるっぽい記述があるな。

ACL2(r) の詳細について知りたくば論文読めもくは著者に問合せてとのことだった。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/COMMON-LISP____REAL

ACL2 にも ACL2(r) という実数が使えるバージョンがあるらしいしまだ ACL2 の可能性は否定できない。

Coq の標準ライブラリに実数があるのか…。https://coq.inria.fr/stdlib/

というか実数が扱えるかどうかが気になる。

うー、ACL2 よりも無限集合に対する証明の方がモチベが高くなっていて ACL2 に執着してはならない気がしてきている……。

探し方を間違えてた。これ ZFC をサポートする定理証明支援系を探せばいのか。

この記事から無限分割の英語版を探して調べるか。https://en.wikipedia.org/wiki/Partition_of_a_set

集合の無限分割で検索してもあんまヒットしないんだがなんでだろう。

集合の無限分割みたいなことを表現できる定理証明支援系があるなら使いたい。

あー、無限を扱いたくなると ACL2 じゃ厳しくなってくるんか。私には教官がいないので証明の正しさを確認してくれる人がいないんで定理証明支援系を使いたい気持ちに駆られている。

なんか行けそうな記事を見つけた。うーん、こういうのみると ACL2 じゃなくて Coq とか Agda とか使いたくなってくるな……。https://zenn.dev/nyolmol/scraps/d886d52541cac4