Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Wednesday, 25-Aug-2021 00:50:02 JST きゅーけー

   Stobj を学んで、これで ACL2 での副作用も楽勝だぜって思ってたらなんか Arrays っていうページもあって困惑している。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____ARRAYS

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Wednesday, 25-Aug-2021 09:50:33 JST きゅーけー

     in reply to

     ACL2 の Arrays は論理的にはただの連想リストなんだけど、特殊な形をした連想リストを制約を守って使うことで実際には配列として処理するものみたい。定理を記述するときは線形時間かかるけど副作用のない扱いやすい連想リストとして使えるが、実際にプログラムを走らせる時には配列として扱われて速いって感じ。