|
--- This is prolog6.doc ---
処理系(CMIS) のデータの側面から見た仕様を述べる。
＜データ構造＞
実行メモリー ------ hnp:(struct thn ノ リスト)
(1) 用途 導出に使うホーン節を置くエリア
外部ファイルとの受渡用にも使われる
(2) 要素
lrmn 仮説から偽でないものを抽出してきた場合その番号
hnt ホーン節
(3) 制御 ユニファイ可能チェックは昇順
hn ホーン節数
h1 現在のゴールのユニファイ相手のホーン節番号
h1p 各ユニファイ回目の h1 のリスト（g1迄）
ゴールヒストリ ---- glp:(struct tgl ノ リスト)
(1) 用途 導出の際、作られるゴール節の履歴
(2) 要素
glt ゴール節（複数アトムからなる）
(3) 制御
g1 現在のゴールのユニファイ回目
gn 現在のゴールのゴールヒストリの番号
g2 現在のゴールのアトム数
h2p 各ユニファイ回目の gn のリスト（g1迄）
h2c 各ユニファイ回目の g2 のリスト（g1迄）
例 pij をゴールのアトムとすると
1 2 3 4 5 6 7 8
1-> 2---------> 3-----> 4----->
p11,p21,p22,p23,p31,p32,p41,p42
g1=4
h2p[g1]=gn=7, h2c[g1]=2
カレントゴール ---- cgp:(struct tcg ノ リスト)
(1) 用途 ユニファイ中のゴール節
(2) 要素
cgt 現在のゴール節（複数アトムからなる）
(3) 制御
g1,hn,h2などはゴールヒストリを参照のこと
例 上図で言えば p41,p42 のこと
言語Ｌメモリー ---- llp:(struct tll ノ リスト)
(1) 用途 言語Ｌ、言語Ｌの文法上のデータを持つ
前提となる節や仮説の制約条件節も持つ
(2) 要素
afc 言語Ｌ等のタイプ＝BLTC/DEFC/DEFP/ATOM/
HEAD/BLTP/FUNC
用途の区別
llvc 変数の数
llat 引数のタイプ＝int/listint/str/liststr
数値、文字、
リストか否か
入力項目か出力項目か等
llt 言語Ｌ等
(3) 制御
usell 言語Ｌ等の数
事実メモリー ------ expp:(struct texp ノ リスト)
(1) 用途 オラクルからの知識で次のものがある
ＭＩＳ実行前に予め教えておく事実
ＭＩＳ実行中オラクルから得る事実
ＭＩＳ実行後、更に要求して得る事実
いずれもＳtrue/Ｓfalseに属す
(2) 要素
tf <a,V> の V つまり真偽
Ｓtrue/Ｓfalseの所属区別でもある
ext <a,V> の a つまり観測文
lrmn この事実（Ｓtrueに属す）の実験で使われた
偽でない仮説の番号のリスト
hnp 中の lrmn を導出に使われた分集めたもの
(3) 制御
useexp 事実の数
仮説メモリー ------ lrmp:(struct tlrm ノ リスト)
(1) 用途 もっぱら精密化により生成された仮説からなるが
言語Ｌメモリーからの前提となる節や仮説の
制約条件節もＭＩＳ実行前に与える。
偽の仮説以外は精密化の対象でない
(2) 要素
fcond 0x01:ADDBODY ENABLE
ftype FINE TYPE 0-5
0 : INIT(NULL CLAUSE())
1 : MKHEAD
2 : SUBSTT HEAD&BODY XI/XJ
3 : SUBSTT HEAD&BODY XI/FY
4 : ADDBODY
5 : BINDBODY
9 : GEN CLAUSE
fmark 仮説の実験の結果判った真偽を持つが
その他に用途で述べた区別を持たせている
HOLD/FIN/IDLE/TRUE/FALSE
cphbvc HEAD & BODY VAR COUNT
cpodr 枝刈り優先順のオーダー（この順序は別記）
cpt 仮説等
(3) 制御 精密化による追加は生成順に後続させる
実験には順にサーチし偽でない仮説を抽出する
精密化すべき偽の仮説の取出は枝刈り優先順に
従いこの順はオーダーに持つ
Ｓtrueの実験後の毎にコンデンスする
usec fmarkがTRUE/IDLEの仮説の数
usecp 仮説等数
sizek サイズｋ
clsa 精密化すべき偽の仮説一つで文Ａのこと
sizea 文Ａのサイズ
useb 精密化（１）～（４）により生成した文Ｂの数
ホーンヒストリ ---- uhp:(struct tuh ノ リスト)
(1) 用途 導出に使われたホーン節をユニファイ後の形で
持たせ、これにより逆導出が可能になる
(2) 要素
uht ユニファイ後のホーン節
(3) 制御
g1はゴールヒストリを参照のこと
g1は即ち uhtの数でもある
＜unify＞ １～ g1 の順にゴールヒストリの生成
（１）仮説メモリー中の偽でない仮説を抽出して実行メモリーに置く
（２）ゴールヒストリ中の現在のゴールを取出してカレントゴールに置く
（３）ユニファイ可能なホーン節を実行メモリーから選択する
（４）カレントゴールとユニファイ可能なホーン節とでユニファイの実行
（５）カレントゴールを取出してゴールヒストリ中の現在のゴールの位置に収める
（６）ユニファイ後のホーン節をホーンヒストリに収める
（７） g1 のインクリメント
＜backtrace＞ g1 ～１ の順にゴールヒストリの置き換え（逆導出）
（１）ゴールヒストリ中の現在のゴールを取出してカレントゴールに置く
（２）対応するユニファイ後のホーン節をホーンヒストリから取出す
（３）カレントゴールとユニファイ後のホーン節とで逆ユニファイの実行
（４）カレントゴールを取出してゴールヒストリ中の現在のゴールの位置に収める
（５） g1 のデクリメント
但し循環導出点の摘出があればユニファイループなので矛盾点追跡させない
逆導出については別記にもあるようにゴールヒストリ・ホーンヒストリと共に用いる
ことにより矛盾点追跡アルゴリズムが非常に簡単になる
＜refinement＞
fmark の遷移でもって説明する
（１）HOLD
・ 前提となる節や仮説の制約条件節
（２）NULL->IDLE
・ 精密化により生成された仮説候補
（３）IDLE->FIN
・ 同一節（variant を含む重複節）である仮説
ある仮説がvariant として他の仮説に存在しているかの
摘出の為に仮説生成時、変数の正規形付替を行っている
例 q(Z,X):-p1(Y,Z),p2(X) は
変数の正規形付替で
q(X,Y):-p1(Z,X),p2(Y) となる
・ 同一のアトムを持つ仮説
これは既約チェックの一部でもある！
例 q:-p1,p2,p3,p2 における p2
・ その他
（４）IDLE->FALSE
・ 精密化（４）により生成した場合、生成時点で即マーク付け
することにより確実に次のステップ以降で精密化の対象になる
・ 閉論理式でないものの一部
ヘッド以外つまりボディに自由変項のみから成るアトムを持つ
仮説
例 q(X,Y):-p1(Z,X),p2(Y),p3(V,W) における p3
・ その他
（５）IDLE->TRUE
・ Ｓtrueの実験後、現時点で真とされた仮説
（６）TRUE->IDLE
・ Ｓtrueの実験前、現時点で真とされた仮説をリセットしIDLE
の状態にする
このことにより今度のＳtrueの実験では使われない仮説となる
可能性のある現時点で真とされた仮説を固定せず帳消しできる
但し変項のない事実節のような自明的な仮定節はリセットせず
・ 一応、真である仮説ではあるが冗長である仮説の可能性があり
その為に精製アルゴリズムを用意してこれを排除することに
した
以 上
|