Home | Notifications | New Note | Local | Federated | Search | Logout

きゅーけー@tojoqk@mastodon.tojo.tokyo

Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバーを運用しています。

Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Agda 学習がメインです。

生活リズムの安定のため、深夜 02:00 から 10:00 までの間はアカウントロックをかけています。その間は何も反応しません。

個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk
Joined: 2025-12-01 20:07:27
190 notes, 1 following, 1 followers

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:57:40)
ACL2がいろんなヒューリスティックを駆使して自動で定理証明するのはまさに実用Common Lispに書いてあるヒューリスティックな探索の話に通じるように思う。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:55:32)
PAIPの日本語訳の実用Common Lispをペラペラと呼んでいた結果、いま自分がACL2を使って定理証明をしているのはかつてのAI研究の成果を享受しているのだということがわかった。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 21:23:17)
@masso 
総称関数の特異点だから特異メソッドと呼んでいたところを、メソッドを関数ではなくメッセージだと考えているシステムに同じ名前のまま別の解釈によって導入した結果なんですね。
結果として目的としても機能としても違うものになっているのにもかかわらず関連づけられているのは奇妙な話ですね…

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-03 20:58:15)
最近Rubyの特異メソッドという概念をしっかりと把握したのだけど、CLOSのeql specializerとはやりたいことが全然違う機能であることがわかった。CLOSの方は特定のシンボルとか数値に対してディスパッチするのがメイン機能であって、eql と equal で意味が変わるようなものを指定するためのものではないと思う。

特異メソッドはCLOSを参考にしたというのは事実なのだと思うけどなんだかCLOSへの誤解をうむのではないかと感じる。。。

きゅーけー@tojoqk@mastodon.tojo.tokyo (2025-12-02 13:42:57)
Emacs の拡張の magit というやつ使ってる