＜知識の帰納的推論＞　ＭＩＳの仕様

ＭＩＳ　：モデル推論（Model Inference）問題を解く、一般的で漸増的アルゴリズム。

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

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

定義　１．未知モデルＭに関する（一階述語）言語Ｌが与えられている。
　　　２．観測言語Ｌｏと仮説言語Ｌｈは言語Ｌに属す。
　　　　　　　Ｌｏ：Ｌのグランドアトム（変数のない項）の集合
　　　　　　　Ｌｈ：Ｌのホーン文の集合
　　　３．観測文（Ｌｏの文）ａの真偽を回答可能な客体をモデルＭに対する神託と言
　　　　　い、そのような神託（＝人間）の存在を仮定する。
　　　　　ＭＩＳにおいて神託に入力を与えその答えを読む操作を実験と呼ぶ。
　　　　　コンピューターが人間に質問し回答を読む操作である。
　　　４．実験の結果の記述を領域Ｍについての事実（＝Ｆｉ）と言い観測文ａと真偽
　　　　　Ｖの対で表す（Ｆｉ＝＜ａ，Ｖ＞でＶ＝true/false）　　
目的　１．事実を読みこみ仮説言語Ｌｈの文の有限集合（＝アルゴリズムの推測：Ｔ）
　　　　　を出力すること。
　　　　　文の集合ＴはＭのＬｏ完全公理化である。（＝事実に対して充分である）
　　　　　ＴはPrologのプログラムに相当する。
　　　　　　　ｈをある全域的な帰納的関数とし
　　　　　　　Ｍを（あるｋ＞０に対して）ｈ従順なモデルとする。
　　　　　　　そのような最小のｋをｋ０とすればｋをｋ０に到達させることにある。
　　　　　ＭＩＳはモデルについて有限個の事実を確かめ、間違った推測を有限回
　　　　　行った後、全ての真なる観測文を導くような真なる仮説の集合を正しく推論
　　　　　する。
　　　　　モデルＭの枚挙が与えられればコンピューターが神託を模倣でき、実験可能
　　　　　になることにより推論の高速化が計れる。

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

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

　　　議論領域　Ｄ：非負整数の集合
　　　一階言語　Ｌ：
　　　　　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
　　　理論（正しい推測）Ｔ
　　　　　le(X,X):-.
　　　　　le(X,s(Y)):-le(X,Y).

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

mis()　　　 spec　ＭＩＳメイン
前提　１．上記、定義の通り。

手順（**は理論と異なる箇所）
　　　ｋ＝0 ，Ｓfalse ＝｛空文｝，Ｓtrue＝｛｝に初期化。
　　　サイズｋ以下の仮説のソース集合をＬﾛｰm(ｋ) とし初期化する。
　　　つまりＬﾛｰm(ｋ) ＝｛空節｝としこの節にfalse マークする。
　　　Ｌﾛｰm はモデルＭのソース集合の近似である。
　　　サイズとはある構造的な複雑さについての尺度でReynoldsの計算式を後述。
　　　仮説は
　　　　　モデルＭで偽なる観測文を導出するときＭに関して強過ぎると言い、
　　　　　モデルＭで真なる観測文を導出できないときＭに関して弱過ぎると言う。
repeat
　　　１．次の事実Ｆｎ：モデルＭの枚挙であるｎ番目の事実＝＜ａ，Ｖ＞を読み、
　　　　　ａをＳtrue又はＳfalse に追加する。
　 repeat
　　　２．１ｓｔ　ｗｈｉｌｅ（推測Ｔが強過ぎる）ｄｏ
**　　　　trueとマーク付けされた仮説（＝Ｌﾛｰm(ｋ) ）により下記のように
　　　　　偽に属すａ（Ｓfalse の元ａ）を導出してみる。
　　　３．ある偽に属すａがｎ回以内の導出で真と導けてしまった時。
　　　　　例外：ｎ回の導出で導けないとき導出打切。（真と導けた扱い）
　　　　　ここの導出回数は制限を課すとループの場合に有害であるのでｎは不使用。
　　　　　backtrace() ：矛盾点追跡（誤った仮説の摘出）
　　　　　　　矛盾点追跡により上記の導出に用いた仮説のあるものがfalse とマーク
　　　　　　　される。
　　　　　全ての偽に属すａがｎ回以内の導出で導けなくなる迄３を繰返す。
　　　４．２ｎｄ　ｗｈｉｌｅ（推測Ｔが弱過ぎる）ｄｏ
　　　　　false とマーク付けされていない仮説により全ての真に属すａが真と導出
　　　　　できるか実験。
**　　　　真に属すａを真と導出するのに用いられた仮説にtrueのマーク付けをする。
　　　５．false とマーク付けされていない仮説により
　　　　　ある真に属すａｉ（Ｓtrueに属すＦｉのａ）が真と導けなかった時。
　　　　　つまり偽と導けたり、例外：最大回以内の導出回数で導けず導出打切
　　　　　となった時。（偽と導けた扱い）
　　　６．false とマーク付けされた仮説を取出し精密化（古い仮説の局所的修正）
　　　　　を試みるために、ｋ＝ｋ＋１。
　　　　　refinement()：精密化＜－サイズｋ以下の仮説の枚挙によりソース集合
　　　　　　　を得る処理。（＝Ｌﾛｰm(ｋ) の生成）
**　　　　（理論では全て真が導けるまで生成仮説で４．の実験を繰り返し、その後
　　　　　　１．を再度検証するが、ここでは実験の前に１．の検証を済ます。）
　 until
　　　７．上記２，４のどちらのｗｈｉｌｅにも入らなくなる迄繰返す。
　　　　　Ｓfalse＝true ＆ Ｓtrue＝false
　　　８．強過ぎることもなく弱過ぎることもない時点でＬﾛｰm(ｋ) を出力する。
　　　　　１へ戻る。
forever

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

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

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

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

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

・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・
　　　　　　　　　　　　　　　　　　　　　　　 １９８８，ＪＵＮ，２８　中村三郎
　　　　　　　　　　　　　　　　　　　　　　** １９９６，ＮＯＶ，２２