Boyer-Moore theorem prover
というのがあるそうで、例えば、PLUS演算の結合性
(EQUAL (PLUS X (PLUS Y Z)) (PLUS (PLUS X Y) Z))
が証明できると書いてある。
こないだのLispは、勿論数学的帰納法が使えないので、上の式を証明することはできないけれど、帰納法の各ステップなら、「殆ど証明可能」
前者も、更に帰納法を使えば証明できる
(lisp '(= (+ 0 (+ J K)) (+ (+ 0 J) K)))
=>(= (+ J K) (+ J K))(lisp '(-> (= (+ I (+ J K)) (+ (+ I J) K)) (= (+ (s I) (+ J K)) (+ (+ (s I) J) K))))
=>true
#'( (= %x %x) . true )
というルールを加えなかったのは、"="は数値の比較のみに限定したいと考えたから。けど、単純な項書き換え系では、データ型の判定はできない。項書き換え系をデータ型付に拡張すればいいんだろうか
Boyer-Moore theorem proverは結構強力で
http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/
によれば、そこそこhardな定理も証明されているらしい。けど、これらは、命題を形式化して放り込んでやれば、答えが返ってくるようなものではなく、人間が無数の補題を用意してやって初めて証明できたんだと思う。そういう意味では、「自動証明」とは程遠い。詳しい原理は知らないけど、多分、基本的には、項書き換えによる等式推論+帰納法なんだと思う。
余代数
余代数というキーワードをあちこちで見かけるので、論文を眺めてみたけど、どういうメリットがあるのか、今一つよく分からなかったり。
(s,t,*)から作られる項代数を考える。*は二項演算で、以下a*bを単にabと書く。そして、やはりいくつかの等式(なんでもいいけど、ssst=tみたいな)が与えられてるとする。要するに、二元生成の半群。閉項の集合は、sとtからなる長さ1以上の有限列の全体と同一視できる。同値類から標準形を取るやり方は、a prioriには存在しないけど、項の間に適当な順序関係を与えて、KBアルゴリズムが停止すれば、項書換えによって、標準形を機械的に得られるようになる。自然数やリストなどは、(自由項代数の)商項代数と見なせるので、項書換えが非常に便利。便利どころか、それで全部の計算ができてしまう。効率は悪いけど
#グレブナー基底も、多項式の同値類から標準形を一つ選ぶ手段を与えるんだった
一方、sとtを記号集合とする、適当な正規表現みたいなのは、sとtからなる有限列の集合ではあるけれど、項書換えみたいな道具を直接使えない。商項代数には、項書換えという強力な道具があるのに、正規表現は単純に項代数と見なすこともできないし、項書換えを利用も出来ない。けど余代数と見ることが出来て、そうしてやると、何かいいことがある、ということなのかもしれない
#全然違うかもしれない。具体的にどう嬉しいのか分からない
#(2006/09/07)
正規表現を余代数と見れるって言い方は変。余代数と見れるのは、(多分)有限オートマトンで、正規表現は、その解と見るのが正確なように思う
http://d.hatena.ne.jp/m-a-o/20060906#p2
