Ex. 4.64
動作を追いかける。見やすくするため、人名、変数は短く書く。
パターン (outranked-by Ben ?w) 規則の結論 (rule (outranked-by ?s-1 ?b-1) ← 規則の変数には連番がつく
ユニファイするとこんなフレームができる。
フレーム ((?s-1 . Ben) (?b-1 . ?w))
このフレームのもとで、規則を作用させる。
つまり、このフレームを入力として規則の本体で パターンマッチ or ユニファイを実行する。
規則の本体
(or (supervisor Ben ?b-1) ①
(and (outranked-by ?m-1 ?b-1) ②
(supervisor Ben ?m-1))) ③
規則の本体①とDBのパターンマッチでできるフレーム
フレーム① ((?s-1 . Ben) (?b-1 . ?w) (?b-1 . Oliver))
ここで、?w が具体的な値に束縛された解が1つみつかった。
規則の本体②とDBのパターンマッチは、また規則の適用になる。①とは OR なので別のフレームストリームになる。
パターン② (outranked-by ?m-1 ?b-1) 規則の結論 (rule (outranked-by ?s-2 ?b-2)) ← 適用ごとに変数に新しい連番がつく
この規則の適用は、
1. outranked-by から自分自身 outranked-by を適用する再帰になっている。 2. さらに、パターンと規則に出てくる変数すべてが未束縛のままである。 このままいくら再帰しても未束縛変数が束縛されない。
このような場合規則の再帰は無限ループになる。
無限ループについて
規則から自分規則への再帰的適用は基本的に無限ループになる。
たとえば
(append-to-form ?x ?y ?z)
と入力すると無限ループになる。
この無限ループを止める条件は
① 入力フレームの変数束縛によってユニファイが失敗すればよい。 ユニファイが失敗すれば規則の本体は実行されない。つまりそのフレームのループは停止する。 (フレームストリームの全フレームでユニファイ失敗すればループは完全に停止する。)
である。
たとえば
(append-to-form (1) (2) (3))
と最初からすべての変数が束縛された状態を入力するとループしない。(式の真偽はともかくループはしない)
本体にDB検索を持つ規則は、DBとのマッチングによって変数束縛すればユニファイ失敗してループを抜けることができる。
(outlanked-by ?x ?y)
は、自己再帰を含むが、?x, ?y がDBで束縛されることでループが止まる。
DB検索のない、ルールだけの規則(append-to-formなど)は、引数で変数束縛すればユニファイ失敗してループを抜けることができる。
(append-to-form ?x ?y (1 2 3))
は ?z の変数束縛が最終的に?x、?yの束縛を引き起こすのでループを抜けることができる。
(append-to-form ?x (3) ?z)
は ?y の変数束縛が ?x, ?z の束縛を引き起こせないので無限ループする。
(append-to-form (1) ?y ?z)
も、無限ループすべきだが、実際はエラーみたいな出力になる。バグかも？
なお
② 本体のない規則
は、そもそもループしない。