<戻る>

<知識の帰納的推論> MISの仕様

MIS :モデル推論(Model Inference)問題を解く、一般的で漸増的アルゴリズム。

     MISはモデルの枚挙からモデルMを極限において推論できる。
     MISは学習システムの一種であり、また例によるプログラム自動合成に
     も適用可能である。

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・

定義 1.未知モデルMに関する(一階述語)言語Lが与えられている。
   2.観測言語Loと仮説言語Lhは言語Lに属す。
       Lo:Lのグランドアトム(変数のない項)の集合
       Lh:Lのホーン文の集合
   3.観測文(Loの文)aの真偽を回答可能な客体をモデルMに対する神託と言
     い、そのような神託(=人間)の存在を仮定する。
     MISにおいて神託に入力を与えその答えを読む操作を実験と呼ぶ。
     コンピューターが人間に質問し回答を読む操作である。
   4.実験の結果の記述を領域Mについての事実(=Fi)と言い観測文aと真偽
     Vの対で表す(Fi=<a,V>でV=true/false)  
目的 1.事実を読みこみ仮説言語Lhの文の有限集合(=アルゴリズムの推測:T)
     を出力すること。
     文の集合TはMのLo完全公理化である。(=事実に対して充分である)
     TはPrologのプログラムに相当する。
       hをある全域的な帰納的関数とし
       Mを(あるk>0に対して)h従順なモデルとする。
       そのような最小のkをk0とすればkをk0に到達させることにある。
     MISはモデルについて有限個の事実を確かめ、間違った推測を有限回
     行った後、全ての真なる観測文を導くような真なる仮説の集合を正しく推論
     する。
     モデルMの枚挙が与えられればコンピューターが神託を模倣でき、実験可能
     になることにより推論の高速化が計れる。

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・

例  二つの数が与えられた場合、大小関係の判定の機能を持つ論理プログラムを
   モデル推論システムで合成させる場合を考えよう。

   議論領域 D:非負整数の集合
   一階言語 L:
     0       非負整数(定数ゼロ)
     s(X)     X の後続要素 (X=X+1) を返す関数
     le(X,Y)    X ≦ Yのとき真,X > Y のとき偽を返す述語
   事実の例
     <le(0,s(0)),true>    (0≦1:真)
     <le(s(0),0),false>   (1≦0:偽)
     <le(s(0),s(0)),true>  (1≦1:真)
     --- etc
   理論(正しい推測)T
     le(X,X):-.
     le(X,s(Y)):-le(X,Y).

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・

mis()    spec MISメイン
前提 1.上記、定義の通り。

手順(**は理論と異なる箇所)
   k=0 ,Sfalse ={空文},Strue={}に初期化。
   サイズk以下の仮説のソース集合をLローm(k) とし初期化する。
   つまりLローm(k) ={空節}としこの節にfalse マークする。
   Lローm はモデルMのソース集合の近似である。
   サイズとはある構造的な複雑さについての尺度でReynoldsの計算式を後述。
   仮説は
     モデルMで偽なる観測文を導出するときMに関して強過ぎると言い、
     モデルMで真なる観測文を導出できないときMに関して弱過ぎると言う。
repeat
   1.次の事実Fn:モデルMの枚挙であるn番目の事実=<a,V>を読み、
     aをStrue又はSfalse に追加する。
  repeat
   2.1st while(推測Tが強過ぎる)do
**    trueとマーク付けされた仮説(=Lローm(k) )により下記のように
     偽に属すa(Sfalse の元a)を導出してみる。
   3.ある偽に属すaがn回以内の導出で真と導けてしまった時。
     例外:n回の導出で導けないとき導出打切。(真と導けた扱い)
     ここの導出回数は制限を課すとループの場合に有害であるのでnは不使用。
     backtrace() :矛盾点追跡(誤った仮説の摘出)
       矛盾点追跡により上記の導出に用いた仮説のあるものがfalse とマーク
       される。
     全ての偽に属すaがn回以内の導出で導けなくなる迄3を繰返す。
   4.2nd while(推測Tが弱過ぎる)do
     false とマーク付けされていない仮説により全ての真に属すaが真と導出
     できるか実験。
**    真に属すaを真と導出するのに用いられた仮説にtrueのマーク付けをする。
   5.false とマーク付けされていない仮説により
     ある真に属すai(Strueに属すFiのa)が真と導けなかった時。
     つまり偽と導けたり、例外:最大回以内の導出回数で導けず導出打切
     となった時。(偽と導けた扱い)
   6.false とマーク付けされた仮説を取出し精密化(古い仮説の局所的修正)
     を試みるために、k=k+1。
     refinement():精密化<-サイズk以下の仮説の枚挙によりソース集合
       を得る処理。(=Lローm(k) の生成)
**    (理論では全て真が導けるまで生成仮説で4.の実験を繰り返し、その後
      1.を再度検証するが、ここでは実験の前に1.の検証を済ます。)
  until
   7.上記2,4のどちらのwhileにも入らなくなる迄繰返す。
     Sfalse=true & Strue=false
   8.強過ぎることもなく弱過ぎることもない時点でLローm(k) を出力する。
     1へ戻る。
forever

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・

backtrace() spec 矛盾点追跡
前提 1.偽のマーク付けされていない仮説により
     ある偽に属すaがn回以内の導出で真と導けてしまった。
手順
   導出の際、作られる次の性質を持つ文の順序付き2分木(成功した unify歴)を
   ゴールヒストリと呼ぶことにする。
     (1)根は空文である。
     (2)全ての葉は仮説またはMで真な観測文であり、どの葉も変数を共有
        しない。(葉はホーン節)
     (3)節点は全て前のゴール節(左成分)と導出に使われたホーン節(右成
        分)の2分導出形である。

   ゴールヒストリを逆にたどり次の手順でMで偽なる仮説(葉であるNi )を摘出
   する。
   1.i=0,N0=2分木の根とする。
   2.今のゴール節を導出した一方(右成分)のホーン節の頭部が
     真の観測文から真と判断できればNi+1 をNi の左成分とする。
     その前のゴール節にゆく。
   3.2で真偽不明ならばNi の反例を作る。
     反例の作成はGreen の代入収集法(今までの代入の合成)による
     Prologの単一化手続きと共有変数の機能により個々の証明中の代入そのもの
     は自動的になされヒストリに保存されている。(変数を含むが)
     従って次の4で変数が一旦、値が定まったならばその後の反例を作るために
     同じ代入を使う必要があることをロジック化することで良い。
   4.神託にホーン節の頭部を例示して真偽を問う。(=実験)
     但し例示に変数が残れば真偽質問前に値を入力してもらう。(最初のみ神託に
     聞くこと)
     真なら2.と同じ
   5.上記2,4においてホーン節の頭部が偽の場合、
     Ni+1 をNi の右成分とする。
   6.i=i+1としNi が葉でなければ2へ戻り追跡を続行する。
     その仮説(葉であるNi に対応する)にfalse のマーク付けをして戻る。

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・

refinement() spec 精密化
前提 1.偽のマーク付けされていない仮説により
     ある真に属すaiが真と導けなかった。
手順
   1.Lローm(k) を生成する為に以下の処理をする。
     偽のマーク付けされている仮説を一つ選びAとする。
   2.文Aに精密化を施すことにより文Bの集合を生成する。
     言語L中のアトムや関数の集合をPとする。
     P={p(X1,X2,--,Xn),q(Y1,Y2,--,Ym),r(Z1,Z2,--,Zu),f(Y1,Y2,--,Yk)等}
     EをPから生成したアトム、
     Fを空又はPから生成したアトムの一つ又は複数として
     文Aは一般的にE:-Fの形である。
     以下の(1)~(4)により文Aにサイズkの非縮小代入を試みる。
     引数のない関数は定数であるが下記代入先に含める必要がある。
     (1)A=空節 ならばB=E:-とする。
     (2)A=E:-Fならば
        B=A{Xi/Xj} とする。
        但しXi,Xj はA中の変数である。(i≠j)
     (3)A=E:-Fならば
        B=A{Xi/f(Y1,Y2,--,Yk)}
        但しXi はA中の変数でありf は言語L中の関数、
          Yj はAに現れないものとする。(Yj の1つにXi は現れて良い)
     (4)A=E:-Fならば
        B=E:-F,G とする。
        但しG=r(Z1,Z2,--,Zu)はP中のアトム、
          ZkはAに現れないものとする。
        またこれには生成時点で直ちに偽のマーク付けをしておく。
**   *(5)A=E:-Fならば
        B=E:-F,G とする。
        但しG=r(Z1,Z2,--,Zu)はP中のアトム、
          ZkはAに現れるもので言語Lに従う拘束を与える。
     以上によりアトム(=原子論理式)による変換,項自由変換(補助述語を持
     つ),文脈自由変換,多重文脈自由変換の結果のいずれの形も得られる。
**    但し、(2)と(3)は節のラストアトムのみに施す。
     また、最汎アトムの採用は頭部のみとする。
   3.上記2により得られた各文Bは次の条件を満足すること。
     (1)文Bは既約であること。
        (精密化はサイズを1ずつ増やしてゆくので既約性検査は事実上しな
        くて良い)
        2.(5)はサイズを1を超えて増やすが文Aに既約なアトムGのみ
        を生成し付加するので差し支えないが精密化(5)は外部からの特別
        な指示(コマンド)かある場合のみ実行できる。
     (2)size(B)=k+1のこと:前のサイズより1だけ増えたもののみ。
        size(B)=Bに含まれる(区切記号を除く)記号の出現回数
               -Bに含まれる異なる変数の個数。
**    (3)閉論理式でない文B等には偽のマーク付けをする。
**       その他、ホーン節としてふさわしくない仮説や言語L仕様でない仮説
        は無効な仮説として仮説の消除を行い仮説数の増加を防ぐ。

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
                        1988,JUN,28 中村三郎
                      ** 1996,NOV,22