Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:34:49 JST きゅーけー

   書くプログラムを一階述語論理の範囲に限定すれば完全性と健全性が保証されるので希望がある。ACL2 はそういう戦略をとってる。そのために課せられた制約はキツいけど使ってる感じなんとかなるという感じはする.。

   • らりお・ザ・何らかの🈗然㊌ソムリエ repeated this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:36:55 JST きゅーけー

     in reply to

     関数が第一級であるということを捨てさえすれば、自動定理証明がそこそこうまくいくのは使ってる感じ結構実感できてる。

     らりお・ザ・何らかの🈗然㊌ソムリエ repeated this.
   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:40:28 JST きゅーけー

     in reply to

     そもそも ACL2 産業界で既に結構使われているし机上の空論ではない。

     https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/?topic=ACL2____INTERESTING-APPLICATIONS

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:45:44 JST きゅーけー

     in reply to

     私が過去に書いたやつでいちばん感動したのは SICP のハフマン符号木まわりの練習問題を ACL2 でやって、ある程度の性質を証明できたときだったと思う。ACL2 用に用意された問題ではない問題でも証明できる体験をすることでモチベーションが上がってきてる。

     https://git.tojo.tokyo/sicp-acl2.git/tree/huffman-tree.lisp

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:46:21 JST きゅーけー

     in reply to

     定理の命名が雑過ぎてよくないなこれ……。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:47:58 JST きゅーけー

     in reply to

     まあ、たしかに現実のソフトウェアと比べれば簡単すぎる例だけど、ハフマン符号化したやつを正しく復号できるとかまで証明できるようになってきたらなんというか面白くなってくるのは分かるっしょ。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:51:42 JST きゅーけー

     in reply to

     関数が第一級じゃなくてもマクロがあればなんとかなる(暴論)。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Friday, 08-Oct-2021 07:55:59 JST きゅーけー

     in reply to

     自動定理証明といっても、補助定理を用意するのは人間でありどんな補助定理を ACL2 に教えればいいかを考えるのは簡単ではないので、実際のところ全然自動じゃないけどね。