Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 10-Apr-2022 00:30:26 JST きゅーけー

   「ACL2 証明」で検索するとマジで私の記事が上の方にでてくるのつらいな。どんだけ人気ないんだ ACL2……。

   なんか楽しいし ACL2 で定理を証明してみて公開していっているんだけど、私にはそれだけ読んで ACL2 を実際に少しでも使えるようになるための学習ができるほどの情報を提供できるスキルがいまのところないんだよな。

   全ての記事に公式チュートリアル読め(本格的なチュートリアルには10~40時間かかるって書いてある)って書いたらそれはそれで ACL2 のモチベ下がりそう。ただ希少情報提供者の責務として全ての記事に公式チュートリアル読めは書いた方がいいかもしれん。

   ACL2 は Lisp と定理証明にめっちゃ興味があるという極稀なケースか何故か ACL2 を使っている研究者や、仕事で実用しているわずかの会社でしか使用されていないわけでなんかライト層を増やすのは無理ゲー感がある。

   なんかどうしようもない気持ちになってる。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 10-Apr-2022 00:35:35 JST きゅーけー

     in reply to

     ACL2 は定理をただ書けばいいわけではなくて定理を書くことで ACL2 をプログラミングする感じなので初見だと意味が分からないんだよな。たとえば、 `(equal x y)` みたいな定理があったとき `(equal y x)` は式としては同じだけど ACL2 の rewrite ルールとしては全然意味が違う(ACL2 は equal の左にあるやつを右に置き換える)とかいうのを知った瞬間にこれは厳しいってなる人はたくさんいるんじゃないだろか……。

     でもその壁を乗り越えるとちょっと関数が複雑になっても定理証明できたりして結構楽しいんだよな。こんな感じでなんか ACL2 で楽しんでいる層を増やして ACL2 界隈を日本に構築したい気持ちがある。