ACL2についてちろっと

数学その他 ACL2

ACL2とはなんぞやということについて全く説明していないので一応。私なぞに解説する権利はないといえばないんですが、日本語での説明がろくにないというか日本語限定でACL2をぐぐるとこのブログがトップなんですが困ったな。たぶんオフィシャルサイトはACL2 Version 6.4。ウィキ先生による解説がACL2 - Wikipedia, the free encyclopedia。まあ要するに定理証明器なんですが、LISPの拡張という面も持っています。nqthmという定理証明器の"industrial strength"を持った拡張版ということらしいです。

The ACL2 programming language is an applicative (side-effect free) variant of Common LISP. ACL2 is unityped. All ACL2 functions are total--that is, every function maps each object in the ACL2 universe to another object in its universe.

えーと、意味もわからずに巡回しているページで出てくる言葉がたくさん混じっているので引用しておきます。

とりあえず適当に使ってみて思う良い点。

  • ベースがLISPなんでわりと読みやすい (正直Coqの出力を読むのは辛かった…)
  • プログラムっぽいアルゴリズムが書きやすい
  • うちの貧弱な環境でもなんとか普通に動いている

悪い点

  • アルゴリズムに関する証明以外に使えるのかがわからない
    • 使えるのかもしれないけど、ドキュメントからなかなか探せない
  • なんだかヒントの与え方がわかりにくい
  • 時々とんでもなくバカなのは仕様ですか？
    • でも逆に妙に賢いときもあるので…

なぜACL2でやり始めたかというと、例のBailey-Cowlesが使っていたからってだけの理由なんですが。とりあえず、たらいまし関数のことをやるにはけっこう良いと思います。ただ、自動証明ということを考えるとやはり自分の専門である集合論のことをやらせたいなと思うわけで、それにつながっていない(かもしれない)というのはちょっといやだなというか初動を間違ったかなというか。