きれいな方法で項の等号と不等号を区別する純粋な Prolog プログラムは、実行の非効率性に悩まされます。関連性のすべての用語が根拠がある場合でも。
SO の最近の例はthis answerです。この定義では、すべての答えとすべての失敗が正しいです。検討：
?- Es = [E1,E2], occurrences(E, Es, Fs).
Es = Fs, Fs = [E, E],
E1 = E2, E2 = E ;
Es = [E, E2],
E1 = E,
Fs = [E],
dif(E, E2) ;
Es = [E1, E],
E2 = E,
Fs = [E],
dif(E, E1) ;
Es = [E1, E2],
Fs = [],
dif(E, E1),
dif(E, E2).
このプログラムは宣言的な観点からは完璧ですが、B、SICStus、SWI、YAP などの現在のシステムで直接実行するのは不必要に非効率的です。次の目標では、リストの各要素に対して選択ポイントが開いたままになります。
?- オカレンス(a,[a,a,a,a,a],M)。 M = [a、a、a、a、a] ; 偽。
これは、次のように s の十分に大きなリストを使用することで確認できaます。Iリストを表示できるように を調整する必要がある場合があります。SWI では、これは次のことを意味します。
1mo はI、次のようなグローバル スタックのリソース エラーを防ぐのに十分小さい必要があります。
?- 24=I,N は 2^I,length(L,N), maplist(=(a),L) です。 エラー: グローバル スタックが不足しています
2do はI、ローカル スタックのリソース エラーを引き起こすのに十分な大きさである必要があります。
?- 22=I,N は 2^I,length(L,N), maplist(=(a),L), ( Length=ok ; 発生数(a,L,M) ). 私= 22、 N = 4194304、 L = [a, a, a, a, a, a, a, a, a|...], 長さ = OK ; エラー: ローカル スタックが不足しています
この問題を克服し、優れた宣言型のプロパティを維持するには、比較述語が必要です。
この比較述語はどのように定義する必要がありますか?
考えられる定義は次のとおりです。
equality_reified(X, X, true). equality_reified(X, Y, false) :- 差分 (X, Y)。
編集:おそらく、ISO組み込みと同様に引数の順序を逆にする必要がありますcompare/3(ドラフトのみへのリンクリンク)。
それを効率的に実装すると、最初に高速で確定的なケースが処理されます。
equality_reified(X, Y, R) :- X == Y, !, R = true. equality_reified(X, Y, R) :- ?=(X, Y), !, R = false. % 構文的に異なる equality_reified(X, Y, R) :- X \= Y, !, R = false. % 意味的に異なる equality_reified(X, X, true). equality_reified(X, Y, false) :- 差分 (X, Y)。
X \= Y編集：制約がある場合に適切なガードであるかどうかは明確ではありません。制約なし、?=(X, Y)またはX \= Y同じです。
例
@ user1638891 で提案されているように、このようなプリミティブの使用例を次に示します。マットによる元のコードは次のとおりです。
occurrences_mats(_, [], []).
occurrences_mats(X, [X|Ls], [X|Rest]) :-
occurrences_mats(X, Ls, Rest).
occurrences_mats(X, [L|Ls], Rest) :-
dif(X, L),
occurrences_mats(X, Ls, Rest).
次のように書き換えることができます。
occurrences(_, [], []).
occurrences(E, [X|Xs], Ys0) :-
reified_equality(Bool, E, X),
( Bool == true -> Ys0 = [X|Ys] ; Ys0 = Ys ),
% ( Bool = true, Ys0 = [X|Ys] ; Bool = true, Ys0 = Ys ),
occurrences(E, Xs, Ys).
reified_equality(R, X, Y) :- X == Y, !, R = true.
reified_equality(R, X, Y) :- ?=(X, Y), !, R = false.
reified_equality(true, X, X).
reified_equality(false, X, Y) :-
dif(X, Y).
SWI の 2 番目の引数のインデックス作成は、 のようなクエリを入力した後にのみ有効になることに注意してくださいoccurrences(_,[],_)。(;)/2また、SWI は、選言にインデックスを付けないため、本質的に非単調な if-then-else を必要とします。SICStus はそうしますが、最初の引数のインデックス付けしかありません。したがって、1 つの選択ポイントが開いたままになります (最後に が付き[]ます)。