チェックが発生する

コンピュータサイエンスにおいて、出現チェックは構文統合アルゴリズムの一部です。これは、 Sが変数Vを含む場合、変数Vと構造体Sの統合を失敗させます。

定理証明において、occusesチェックなしでの単一化は、不健全な推論につながる可能性があります。例えば、Prologの目標 ${\displaystyle X=f(X)}$ 成功すると、X はHerbrand の宇宙には対応するものがない循環構造に結び付けられます。別の例として、^{[ 1 ]} 出現チェックなしで、非定理^{[ 2 ]}の分解証明を見つけることができます。${\displaystyle (\forall x\exists yp(x,y))\rightarrow (\exists y\forall xp(x,y))}$その式の否定は連言標準形を持つ${\displaystyle p(X,f(X))\land \lnot p(g(Y),Y)}$、 と${\displaystyle f}$そして${\displaystyle g}$それぞれ、第１および第２の存在量化子に対するスコレム関数を表します。 チェックがない場合、リテラル${\displaystyle p(X,f(X))}$そして${\displaystyle p(g(Y),Y)}$これらは統合可能であり、反駁する空節を生成する。

Prologの実装では、効率上の理由からoccussチェックを省略することが多いが、これは循環データ構造やループにつながる可能性がある。occussチェックを行わないことで、項を統一する際の最悪ケースの複雑さは $t1$用語付き$t2$ 多くの場合、 ${\displaystyle O({\text{size}}(t_{1})+{\text{size}}(t_{2}))}$ に ${\displaystyle O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))}$; 変数項の単一化が頻繁に行われる場合、実行時間は縮小します。 ${\displaystyle O(1)}$[ ^{注1 ]}

ColmerauerのProlog IIに基づく実装 ^{[ 4 ] [ 5 ] [ 6 ] [ 7 ]}は、 有理木統合を使用してループを回避します。しかし、循環項が存在する場合、複雑時間を線形に保つことは困難です。Colmerauerのアルゴリズムが2次になる例^{[ 8 ]}は容易に構築できます。

ジャファールの1984年の研究では、ユニオンファインド技術に基づく改良が提案され、^{[ 9 ]}最悪ケースの複雑さをほぼ線形時間に効果的に削減しました。SWI-Prolog、 SICStus Prolog、Scryer Prolog、Ciao Prologなどの現代のシステムは、このアプローチのバリエーションを実装しているようです。

統一アルゴリズムの実行例については、画像を参照してください。統一（コンピュータサイエンス）#統一アルゴリズム、目標を解決しようとしています${\displaystyle cons(x,y){\stackrel {?}{=}}cons(1,cons(x,cons(2,y)))}$ただし、発生チェックルール（ここでは「check」と名付けられている）がない場合、代わりにルール「eliminate」を適用すると、最後のステップで循環グラフ（つまり無限項）が発生します。

ISO Prologの実装には健全な単一化のための組み込み述語unify_with_occurs_check/2がありますが、それ以外の方法で単一化が呼び出される場合は、アルゴリズムが「occurs-checkの対象とならない」（NSTO）すべてのケースで正しく動作する限り、健全でないアルゴリズムやループアルゴリズムを使用しても構いません。^{[ 10 ]}組み込みのacyclic_term/1は、項の有限性をチェックするために使用されます。

すべての統合に対して健全な統合を提供する実装は、Qu-PrologとStrawberry Prologであり、(オプションでランタイム フラグを介して) XSB、SWI-Prolog、CxProlog、Tau Prolog、Trealla Prolog、Scryer Prologです。さまざまな ^{[ 11 ] [ 12 ]}最適化により、一般的なケースで健全な統合が可能になります。

WP Weijland (1990). "Occurチェックなしの論理プログラムの意味論" .Theoretical Computer Science.71 : 155–174.doi : 10.1016 / 0304-3975 (90)90194-m .