語句の真相とあやまち

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

これからしたいこと

  • 真偽値が確率であるような論理を考える
  • 時間によって変化する公理系の満たすべき条件を考える
  • 命題論理との融合(?)
    • 命題レベルで全証明をとらえて(SAT solverなのか)
    • それを制約条件として一階の全証明(=mgu)をとらえる
  • そのとき、 P \lor  \neg{P}は命題レベルでは見えなくなること・・・

ニューラルネットで個体という概念を学習できるのだろうか

ニューラルネットで画像認識をした場合、二つの像が似ていることは学習できるけれど、その二つの像の示す個体の同一性までは学習できていないと思う。

 

たとえば、セキュリティで同じ人間かどうかは判定するとき、顔や指紋に基づいて処理するが、それは同一人物であるということを学習しているわけではない。ようだ。

 

同一性という概念はあいまいで難しいから人間でもわからなくなる。

 

その部分は人間がプログラムを組んでいるのだろうけれど、

量子計算と論理について考え始める

ある像aがNNでカテゴリーPに属する確率をrと判定されたとき、P(a,r)と書くとすると事実は+P(a,r)として得られる。

では-P(a,1-r)なのかというと違うような気がする。

否定と確率の関係を理解するために、あれこれ考えているうちに、量子計算が関係するかもしれないと思いこの本を読み始めた。量子コンピュータ入門(宮野, 古澤)。

最近、数理科学でも量子情報の特集があったりしていて、ブームに押し流されているのかもしれない。

 

この本を読んでいて、4章のあたりで論理ゲートのふるまいの説明を読んで書いてあることの意味が分からなくなったのだけれど、|0>=1|0>+0|1>と|1>=0|0>+1|1>の定義にもどって考えなくてはならないことに気づいたら、先に進むことができた。

 

 

今後したいことの整理

  1. 確率と否定
    1. P(a,r) でrをP(a)である確率だとする。
    2. このとき、¬P(a,r)はP(a,1-r)と同じではないみたいだ。
    3. ¬P(a,1-r)を含めた四つの関係は?
  2. 量子計算-トポス-論理-確率と否定
  3. 全proofの有限表現と操作
    1. 証明のカバリング
    2. proofの情報とはなにか?
      1. Capical変数なのか?
  4. 時間によって変化するAxiomと自動証明
    1. A=>A' のときTh(A)=>Th(A')はどう対応するのか
    2. Aに対して、+a, -a, -a+b
  5. Resolution
    1. よいrenameとは?
      1. unification
      2. substitution
      3. 情報抽出
      4. 証明
    2. literl evaluation
    3. term evaluation/partial
    4. rid,cidの有効性は?
    5. varidの扱いは?
    6. templateといってていいのか?
    7. 実装について
      1. literal, clause, termをjuliaのExprにしていていいのか? parserを作らなくていいのか
      2. timeoutをいれてはどうか
      3. 必要なloopのみ実行できるようにしたい
  6. NN
    1. NNでLogicにたどりつけるのか
      1. たとえば、三段論法を学習できるのか。
      2. 例) 同一性を学習できるか
        1. 像が似ていることは判定できても、それの背景に同じ個体があることを学習できるのか。 双子の問題とか
        2. 力学では、量質が同じ物体は区別されないというようなこともあり、同一性とは何か
        3. 同じとはどういう意味か
        4. そもそもNNで学習するとはどういうことか?
      3. 音と像をあわせてNNで学習すると、音と像の対応関係が学習されるのか
        1. 楽器の写真を見せるとその音がわかったり、音を聞かせると楽器の写真がわかったり?
        2. それができるのなら、声から人物を特定することができるのか
      4. NNとLogicを繋ぐことの意味
        1. NNでLogicまで学習するのはコストが高すぎる
        2. すべてをAIでできるということ
  7. 具象と抽象の間をいききできる
    1. P(x,r)とφ(P,x,r)が同値だとすると、いろいろできる
    2. そのとき証明のloopを抑制する必要がある。必要のないloopをしないですませる方法は?

λ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))

の証明は当然できる。