Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Wednesday, 01-Sep-2021 22:16:29 JST きゅーけー

   頼まれごとして簡単なプログラムを書いたんだけど、最初は ACL2 でやろうとして、ちょっと時間かかりそうだったので GNU Guile、って思ったけど最終的に Racket で解いてしまった。battery included の便利さを実感してしまった。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Wednesday, 01-Sep-2021 23:37:43 JST きゅーけー

     in reply to

     さっきの頼まれごとの正体は文字列のリストから n 個を取りだす全ての組合せを求めて欲しいというものだったんだけど、ACL2 で実装した。とりあえず組合せの数に関する定理を書いたら補助定理なしで自動証明できてしまって驚いた。

     コード: https://git.tojo.tokyo/acl2-theorems.git/tree/combinations.lisp?id=975418f4c2e1520649196458d3211e6ef9ec531aACL2 の出力: https://ci.tojo.tokyo/jobs/acl2-verify/412

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Wednesday, 01-Sep-2021 23:39:19 JST きゅーけー

     in reply to

     たしかに、combinations 関数と comb 関数は似ているので、自動証明できるのはそんなに不思議な話ではない気もする。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Wednesday, 01-Sep-2021 23:41:11 JST きゅーけー

     in reply to

     でも、(len (cons-all e x)) が (len x) と等しいとかは証明してないのに自動証明されたのは今までの感覚とはちょっと異なる。やっぱり ACL2 の振舞いについてまだまだ分かってないことがあるな。