prolog - 要約 - 人間不平等起源論 講談社
期限平等/不平等の証明 (4)
この述部を同じ引き数(=)/3呼び出すのが最善のようです。 このように、 if_/3ような条件ははるかに読みやすくなりました。 そして、 _truth代わりに接尾辞_tを使用するには：
memberd_t(_X, [], false).
memberd_t(X, [Y|Ys], Truth) :-
if_( X = Y, Truth=true, memberd_t(X, Ys, Truth) ).
これまでに使用されていた：
memberd_truth(_X, [], false).
memberd_truth(X, [Y|Ys], Truth) :-
if_( equal_truth(X, Y), Truth=true, memberd_truth(X, Ys, Truth) ).
平等と不平等をクリーンな方法で区別する純粋なPrologプログラムは、実行の非効率性に苦しんでいます。 関連性のあるすべての条件が満たされても
最近のSOの例はこの答えです。 この定義では、すべての回答とすべての失敗が正しいです。 検討してください：
?- 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などの現在のシステムでの直接実行は不必要に非効率的です。 次の目的のために、リストの各要素に対して選択点が開いたままになります。
?- occurrences(a,[a,a,a,a,a],M). M = [a, a, a, a, a] ; false.
これは、以下のようにa sの十分に大きなリストを使用することで確認できます。 リストをまだ表現できるようにIを適応させる必要があるかもしれません。 SWIでは、これは
1m Iは、次のようなグローバルスタックのリソースエラーを防ぐのに十分な大きさでなければなりません：
?- 24=I,N is 2^I,length(L,N), maplist(=(a),L). ERROR: Out of global stack
2do Iはローカルスタックのリソースエラーを引き起こすのに十分な大きさでなければなりません：
?- 22=I,N is 2^I,length(L,N), maplist(=(a),L), ( Length=ok ; occurrences(a,L,M) ). I = 22, N = 4194304, L = [a, a, a, a, a, a, a, a, a|...], Length = ok ; ERROR: Out of local stack
この問題を解決し、優れた宣言プロパティを保持するには、いくつかの比較述語が必要です。
この比較述語はどのように定義する必要がありますか？そのような可能な定義は次のとおりです。
equality_reified(X, X, true). equality_reified(X, Y, false) :- dif(X, Y).
編集：おそらく引数の順序は、ISOの組み込みのcompare/3 （草案のみへのリンクリンク）と同様に逆にする必要があります。
それを効率的に実装することで、まず迅速に決定されるケースを処理できます。
equality_reified(X, Y, R) :- X == Y, !, R = true. equality_reified(X, Y, R) :- ?=(X, Y), !, R = false. % syntactically different equality_reified(X, Y, R) :- X \= Y, !, R = false. % semantically different equality_reified(X, X, true). equality_reified(X, Y, false) :- dif(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).
occurrences(_,[],_)ようなクエリを入力すると、SWIの2番目の引数のインデックスが有効になることに注意してください。 また、SWIは本質的に非単調のif-then-elseを必要とします。なぜなら、それは(;)/2 - disjunctionでインデックス付けしないからです。 SICStusはこれを行いますが、最初の引数インデックスのみを持ちます。 そのため、1つの選択ポイントが開いたままになります（最後は[] ）。
まあ、あるものの、 equality_truth/2ように、その名前はもっと宣言的でなければなりません。
更新：この回答は4月18日の鉱山に取って代わられました。 私はそれが以下のコメントのために削除されることを提案しません。
私の以前の答えは間違っていた。 次のものは質問のテストケースに対して実行され、実装には余分な選択肢を避けるという望ましい機能があります。 私はトップ述語モードを？、+、？と仮定します。 他のモードも容易に実現することができる。
プログラムには4つの句があります。第2引数のリストが訪問され、各メンバーには2つの可能性があります。上位述語の第1引数と統合するか、または異なる場合はdif制約が適用されます。
occurrences(X, L, Os) :- occs(L, X, Os).
occs([],_,[]).
occs([X|R], X, [X|ROs]) :- occs(R, X, ROs).
occs([X|R], Y, ROs) :- dif(Y, X), occs(R, Y, ROs).
YAPを使ったサンプルラン：
?- occurrences(1,[E1,1,2,1,E2],Fs).
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
E1 = 1,
Fs = [1,1,1],
dif(1,E2) ? ;
E2 = 1,
Fs = [1,1,1],
dif(1,E1) ? ;
Fs = [1,1],
dif(1,E1),
dif(1,E2) ? ;
no
?- occurrences(E,[E1,E2],Fs).
E = E1 = E2,
Fs = [E,E] ? ;
E = E1,
Fs = [E],
dif(E,E2) ? ;
E = E2,
Fs = [E],
dif(E,E1) ? ;
Fs = [],
dif(E,E1),
dif(E,E2) ? ;
no
次のコードは、AUBUCのProlog共用体で@falseによって実装されているif_/3および(=)/3 （別名equal_truth/3 ）に基づいています。
=(X, Y, R) :- X == Y, !, R = true.
=(X, Y, R) :- ?=(X, Y), !, R = false. % syntactically different
=(X, Y, R) :- X \= Y, !, R = false. % semantically different
=(X, Y, R) :- R == true, !, X = Y.
=(X, X, true).
=(X, Y, false) :-
dif(X, Y).
if_(C_1, Then_0, Else_0) :-
call(C_1, Truth),
functor(Truth,_,0), % safety check
( Truth == true -> Then_0 ; Truth == false, Else_0 ).
occurrences/3と比較すると、補助occurrences_aux/3は、リストEsを最初の引数として渡す異なる引数の順序を使用します。これにより、最初の引数のインデックス付けが有効になります。
occurrences_aux([], _, []).
occurrences_aux([X|Xs], E, Ys0) :-
if_(E = X, Ys0 = [X|Ys], Ys0 = Ys),
occurrences_aux(Xs, E, Ys).
occurrences_aux(_,E,Fs)は、@migfilgによって指摘されているように、 Fsすべての要素が等しいと宣言しているため、 Fs=[1,2], occurrences_aux(Es,E,Fs) E 。 しかし、それ自体では、このような場合にはoccurrences_aux/3は終了しません。
補助述語allEqual_to__lazy/2を使用して終了動作を改善することができます。
allEqual_to__lazy(Xs,E) :-
freeze(Xs, allEqual_to__lazy_aux(Xs,E)).
allEqual_to__lazy_aux([],_).
allEqual_to__lazy_aux([E|Es],E) :-
allEqual_to__lazy(Es,E).
すべての補助述語を適所に置いて、 occurrences/3定義しましょう：
occurrences(E,Es,Fs) :-
allEqual_to__lazy(Fs,E), % enforce redundant equality constraint lazily
occurrences_aux(Es,E,Fs). % flip args to enable first argument indexing
いくつかの質問をしましょう：
?- occurrences(E,Es,Fs). % first, the most general query
Es = Fs, Fs = [] ;
Es = Fs, Fs = [E] ;
Es = Fs, Fs = [E,E] ;
Es = Fs, Fs = [E,E,E] ;
Es = Fs, Fs = [E,E,E,E] ... % will never terminate universally, but ...
% that's ok: solution set size is infinite
?- Fs = [1,2], occurrences(E,Es,Fs).
false. % terminates thanks to allEqual_to__lazy/2
?- occurrences(E,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1], E=1 ;
Fs = [2,2], E=2 ;
Fs = [3,3], E=3 ;
Fs = [], dif(E,1), dif(E,2), dif(E,3).
?- occurrences(1,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1]. % succeeds deterministically
?- Es = [E1,E2], occurrences(E,Es,Fs).
Es = [E, E], Fs = [E,E], E1=E , E2=E ;
Es = [E, E2], Fs = [E], E1=E , dif(E2,E) ;
Es = [E1, E], Fs = [E], dif(E1,E), E2=E ;
Es = [E1,E2], Fs = [], dif(E1,E), dif(E2,E).
?- occurrences(1,[E1,1,2,1,E2],Fs).
E1=1 , E2=1 , Fs = [1,1,1,1] ;
E1=1 , dif(E2,1), Fs = [1,1,1] ;
dif(E1,1), E2=1 , Fs = [1,1,1] ;
dif(E1,1), dif(E2,1), Fs = [1,1].
編集2015-04-27
いくつかのケースでは、 occurrences/3 universalが終了するかどうかをテストするクエリがいくつか追加されています。
?- occurrences(1,L,[1,2]).
false.
?- L = [_|_],occurrences(1,L,[1,2]).
false.
?- L = [X|X],occurrences(1,L,[1,2]).
false.
?- L = [L|L],occurrences(1,L,[1,2]).
false.