語句の真相とあやまち

なにもないことにまつわるあれこれとか関係のないこととか

λx,z,E.y F(x,y),F(y,z)→F(x,z)

clause形に変換するとき、違うclauseの変数は独立になる。

 

λx,z,E.y F(x,y),F(y,z)→F(x,z)

は、全順序のようにも見えるが本当は、友達の友達は友達の関係。

ここでは、yが存在すればF(x,z)であるということで、存在が重要。

 

存在を全称にしてしまってこれをclauseにすると

¬F(x,y),¬F(y,z),F(x,z)

となり、これの否定は

F(x,y),F(y,z),¬F(x,z)

になる。

この否定が矛盾を導けば、元の主張は正しいということになる。

 

Fact1={F(a,b), F(b,c),F(a,c)}

のとき、確かに反証できる。

しかし、

Fact2={F(a,b), F(d,c), F(a,c)}

でも成り立ってしまうのはおかしい。

これはおそらく、yは存在なのでclauseを超えて同じ値にならなくてはならないということではないだろうか。

 

もともとclause formにするとき存在変数は定数に置き換えられることになるので、同一性は必要とされる。しかし、定数では代入ができないのでこの問題が解決できない。

 

mguを代入とだけ考えるのではなく、{x←t}を{x=t}という条件と考えれば、対処できるとは思う。

 

いずれにせよ、存在変数(とは呼ばないと思うが)は、clauseを超えた変数の同一性と考えればいいのではないか。

 

あるいは問題の視点が間違っているかも。

 

 

 

 

Factのadjustについて

Factの述語記号P、定数記号cとし、FactにP(c)が含まれていないとき

 

  • Pが2つに一つだったら、-P(c)を加えてもいいはず。
    つまり、G(x)が'xは少女'という意味なら、FactにG(c)が含まれていなければ'-G(c)'にしても、だいたい正しい
  • 一方で、友達を表す'F(x,y)'について、Factの中で、F(a,b), F(b,c)からF(a,c)が導けるかどうかを判定しようとしてるときに、勝手にF(a,c)を加えてはならない。

こんな証明はできないのか

clauseの集合を

{P(a), Q(a), Q(b)}

としたとき

any x. P(x) → Q(x)

は証明できるのか?

 

できないみたい。

Herbrand Universeで成り立っても、必ずしも成り立たないようなかんじ。

 

もしも、

{P(a), P(f(x))}

P(f(x))

の証明は当然できる。

 

 

そしてResolution

Juliaで論理式を表す方法について、ずっと試行錯誤している。

いまは、parse("[x,y].[+P(x,f(x)),-Q(x,y)]") のようにparse()を使うことにして、Exprベースで式を扱っている。

内部で[x,y] と :([+(P(x,f(x)),-(Q(x,y))] に分けているのだけれど、これも[:(+(P(x,f(x)))), :(-(Q(x,y))]にしたほうがいいかもしれない。

 

Resolutionについては、だいぶ忘れてしまったので、思い出すためにいろいろ調べているけれど、今のAIブームの中では自動証明はほとんど話題になっていないように見える。

 ニューラルネットと自動証明はAIの両輪のような気がするけれど、そうでもないのかもしれない。そもそもAIという言葉も意味不明ではあるけど。

 

話題がそれたので戻すと、unificationはできていて、単体のResolutionもできているはず。

あとはclause集合からcontradictionを導出するtactics/strategyをどうするか・・・

 

まず、命題論理でgoalからの証明の枠組みを作り、一階でその証明にmguが存在するかどうかでステップの刈り込みを行う。

このとき、繰り返される証明ステップパターンが無限の証明になるのをどうするか。

 

これは先の場合と同じく、

  • 世界の事実(Fact)をground unit clauseの集合で表し
  • それに対する仮説(理論, Theory)を変数を含むclauseの集合で表す
  • queryはいまのところunit clauseを想定

というようなもの。

仮説は、すべてのFactについて成立するものを考えているので、少なくとも

Fact + Theory は無矛盾にしたい。これは、Theoryの各clauseをFactに加えたとき矛盾がでないことで分かるが、たぶん有限時間に検証できるだろう。

複数のTheoryの間の矛盾は有限時間では分からないかもしれない。たぶん分からない。

 

 

 

それから Resolutionにいたるまで

JuliaでResolutionをしたいと思っていたのだけれど、式の表現でSymbolを使うといちいち:なんとかと書かなくてはならないことや、Lispだとlistにするところをベクトルにした場合の表現方法などで悩んで、手がつかなかったのが、去年のどこかでそのあたりがわかったので、いろいろとプログラムを作っている。

最初に作ったのは、非常に単純なものというか制限をつけたもので、それがだいたいできた段階で、真面目に1階述語のResolutionを作った。

 

今は、Unit resolutionあるいはLinear Resolutionで証明(あるいは反証)を作るあたりを考えている。

 

最初に作ったものでは

1. 世界の事実を記述したUnit Clauseの集合に対して、Queryとしての論理式が与えられると、その変数に対する代入を解=モデルを求めるというもの。

DBのQueryみたいなものだ(歴史的には逆か)

 

事実は変数を含まないので、resolutionも一方向の代入だけを考えればよく、事実の全Factを列、QueryのClauseの各Literalを行とし、成分にmguをとるような行列を考える。

その行列を元に、代入の積を使ってQuery全体で成立するモデルを絞り込むというようなもの。

いくつかサンプルをやってみると、あまり深い答えはでなかった。

これはこれで面白いのだけれど、まともな一階述語論理のシステムにしてみようと思うようになったという次第。

 

計算のこと

クラスにもとづくオブジェクト指向は、計算というか関数を整理するための仕組みだと思う。前にも書いたかもしれない。

 

同じアルゴリズムオブジェクト指向で書いたり、Cで書いたりして、それを同じアルゴリズムだと区別できるのだから、そういうことだろう。

 

COMMON LISPのgeneric functionやその他、型ベースでメソッドをディスパッチするタイプのオブジェクト指向(というよりただの型か)の方式もそう見られる。

 

計算の方式自体が違うとしても、時系列上で実行される処理が同じなのだから、それは計算の表現の違いと考えるべきで、結局、こまぎれにしたメソッドをどう管理するかという問題だと見られる。

 

Apple Dylanの開発環境では、メソッドをデータベースで管理していたけれど、まさにそういうことではないのだろうか。

 

 

Project EulerをJuliaでやる

Projct EulerをJuliaで解いてみる。

以前は、RubyかRかで20個くらい解いたあと、問題が面倒臭いのばかりで放棄していたのだけれど、途中で言語を変えるのもおもしろくないから、改めてJuliaで解くためにアカウントを新調してみた。

 

解法をブログに書くのは問題があるのでしないけれど、思ったことなどをここに書くことにしよう。

 

問題1を解いて思ったのは、私にとってプログラムまたはプログラミングとは、問題あるいは解法を明瞭に記述することのようで、手順で書くよりも関係で書くほうを好んでいるらしい。ちがうかもしれない。

 

問題11までは、すぐに答えがでたのだけれど問題12は時間がかかっている。これはプログラムの実行時間のこと。

 49.8分かかった。

 

プログラムを書くまでにかかる時間は、問題にもよるわけで、もしもJuliaやそのパッケージで使えるものがあれば使っているので、ときどき、問題の意図と違う解法をしているのかと思わなくもないけれど、違う言語を使うと言うことはそういうことだと思う。細かいアルゴリズムで解きたくなることもあるので、そういうときはそうするかもしれない。