なぜswiplからの一貫性のない応答？

Question

swiplとのやりとりが矛盾しているように見える理由を理解したいと思います。

これは典型的な例です。私は、以下の定義が含まれてナレッジベースを相談しているとします

私は私の画面は、私はプロンプトで max([0, 1, 2], X).を入力した後にどのように見えるかを示し、そして は Enterを押し下

acc_max([H|T], A, Max) :- H > A, acc_max(T, H, Max). 
acc_max([H|T], A, Max) :- H =< A, acc_max(T, A, Max). 
acc_max([], A, A). 

max([H|T], Max) :- acc_max(T, H, Max). 

：

?- max([0, 1, 2], X). 
X = 2 ▮ 

（ ▮は、カーソルの位置を示す。）

注、特に、インタープリタの次のプロンプトがまだ現れていないこと。ここで

は私がを入力した後、画面が次のようになります。：

?- max([0, 1, 2], X). 
X = 2 ; 
false. 

?- ▮ 

今、私は最終的にインタプリタのプロンプトを取得します。これとは対照的に

、私は私の画面は、私はプロンプトでmax([2, 0, 1], X).を入力した後にどのように見えるかを示し、およびを打つを入力下回っ：この時間は、私はすぐに通訳者のプロンプトを得たことを

?- max([2, 0, 1], X). 
X = 2. 

?- ▮ 

お知らせ - 私がやりました入力する必要はありません;。また、falseもありません。

私は（例えば、時には出力true.は、画面上に示しているが、他の同様の状況ではない）他の多くの同様の矛盾を見つけました。プロローグに新人として

、私はそのような矛盾が（彼らは、私は本当に何が起こっているの見当もつかないを持っていないことを一定のリマインダーであることから、落胆言及しないように）当惑を見つけます。

これらの矛盾を合理化するための簡単な方法はありますか？

また、SWI-Prologのはよりも、より一貫性と予測可能な相互作用を提供プロローグの一部の実装はありますか？

Answer 1

@lurker前記ように、これは、選択点の結果である - より多くのソリューションをもたらすことができる評価されていないルールがある場合、。

例のさらに簡単なバージョンmax([0,1],X).対max([1,0],X).を見てみましょう。

max([0,1],X).：

これは、両方のacc_max([H|T], A, Max) :-ルールにマッチする、acc_max([1],0,X).に行きます。

最初に1 > 0が真であることを確認し、acc_max([],1,X)と呼び出します。これはacc_max([], A, A).にのみ一致し、したがってXと1を1に統一します。解決策があります！しかし、まだ評価されていないルールもあります。あなたが見るところである：

X = 1 ▮ 

は、だから今、私たちはを入力します。を入力し、2番目のacc_max([H|T], A, Max) :-のルールを評価します。 1 =< 0は真ではないので、このルールは失敗します。私たちは今試してみるべきルールから外れているので、それ以上の解決策はありません。したがって：

X = 1 ; 
false. 

今、私たちはmax([1,0],X).を見てみましょう：

これは今acc_max([0],1,X).です。繰り返しますが、表示される順序で評価される2つのルールがあります。

最初に0 > 1が真でないことがわかります。最初のルールは失敗し、2番目のルールが評価されます。

ここで0 =< 1が真であることがわかり、acc_max([],1,X)を呼び出します。これはacc_max([], A, A).にのみ一致するため、Xを1（1回）と統一します。私たちには解決策があり、今度は未評価のルールはありません（つまり、未選択の選択肢はありません）。だから今、私たちは以下を参照してください。

X = 1. 

...他の解決策が存在しないことをプロローグの「心」の疑いがあるとして。規則の順序を逆にする場合：

acc_max([], A, A). 
acc_max([H|T], A, Max) :- H =< A, acc_max(T, A, Max). 
acc_max([H|T], A, Max) :- H > A, acc_max(T, H, Max). 

...このような振る舞いも見えます。

これはがであり、一貫した予測可能なやりとりであり、Prologのすべてのバリアントが共有するものであることを証明するのに役立ちます。