最初のマイナーな問題: の一般的な定義でplus/3は、1 番目と 2 番目の引数が交換されているため、1 番目の引数のインデックス作成を利用できます。Art of Prolog のプログラム 3.3 を参照してください。これも以前の投稿で変更する必要があります。私はあなたの交換された定義plusp/3とあなたの最適化された定義を呼びますpluspo/3。したがって、与えられた
plusp(X, 0, X) :- 自然数(X).
plusp(X, s(Y), s(Z)) :- plusp(X, Y, Z).
レッドカットの検出 (質問 1)
レッド/グリーンカットを証明または反証する方法は? まず第一に、ガード内の「書き込み」統合に注意してください。つまり、カット前のそのような統合の場合です。最適化されたプログラムで:
pluspo(X, Y, X) :- (Y == 0 -> ! ; Y = 0), (X == 0 -> ! ; true), ...
私は次のことを見つけます：
pluspo(X, Y, X) :- (...... -> ! ; ... ), ...
では、反例を考えてみましょう。このカットを赤い方法でカットするには、「書き込み統合」が実際のガードをY == 0真にする必要があります。つまり、構築するゴールには何らかの形で定数 0 が含まれている必要があります。考えられる可能性は 2 つだけです。最初または 3 番目の引数。最後の引数のゼロは、多くても 1 つの解しかないことを意味し、それ以上の解を切り捨てる可能性はありません。したがって、最初の引数には 0 を指定する必要があります。(2 番目の引数は、最初から 0 であってはなりません。そうしないと、「書き込みの統合が悪影響を与えることはありません。」) そのような反例の 1 つを次に示します。
?- pluspo(0, Y, Y).
これにより、1 つの正しい解が得られますY = 0が、他のすべての解が隠されます。だから、ここにそのような邪悪な赤いカットがあります！そして、無限に多くの解を与える最適化されていないプログラムとは対照的です。
Y = 0;
Y = s(0) ;
Y = s(s(0)) ;
Y = s(s(s(0))) ;
...
したがって、あなたのプログラムは不完全であり、それをさらに最適化することについての質問は関係ありません。しかし、もっとうまくやることができます。最適化したい実際の定義をもう一度言いましょう。
plus(0, X, X) :- 自然数(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
実質的にすべての Prolog システムでは、最初の引数のインデックス付けがあり、次のクエリを確定します。
?- plus(s(0),0,X)。
X = s(0)。
しかし、多くのシステムは (完全な) 3 番目の引数のインデックス付けをサポートしていません。したがって、SWI、YAP、SICStus で取得します。
?- プラス(X, Y, 0).
X = Y、Y = 0 ;
偽。
おそらく書きたかったのは次のとおりです。
pluso(X, Y, Z) :-
% パート 1: グリーン カット
( X == 0 -> ! % 最初の引数のインデックス付け
; Z == 0 -> ! % 第 3 引数の索引付け。例: Jekejeke、ECLiPSe
; 真実
)、
% パート 2: 元の統合
X = 0、
Y = Z、
自然数(Z)。
pluso(s(X), Y, s(Z)) :- pluso(X, Y, Z).
との違いに注意してくださいpluspo/3: 現在はカット前のテストのみです! すべての統一はその後です。
?- pluso(X, Y, 0).
X = Y、Y = 0。
これまでの最適化は、2 つの節のヘッドの調査のみに依存していました。彼らは再帰規則を考慮していませんでした。そのため、グローバルな分析なしで Prolog コンパイラに組み込むことができます。オキーフの用語では、これらのグリーン カットはブルー カットと見なされる場合があります。The Craft of Prolog、3.12を引用するには:
ブルーカットは、Prolog システムに、気付くべきであるが気付かない決定性を警告するためにあります。ブルー カットは、プログラムの目に見える動作を変更するものではありません。実行可能にするだけです。
グリーンカットは、成功する、無関係である、または失敗するにちがいない証明の試みを排除するためにありますが、Prolog システムがそれを判断できるとは思わないでしょう。
ただし、重要なのは、これらのカットが適切に機能するにはガードが必要だということです。
ここで、別のクエリを検討しました。
?- pluso(X, s(s(0)), s(s(s(0))))。
X = s(0) ;
偽。
または、より単純なケースに入れます:
?- pluso(X, s(0), s(0))。
X = 0;
偽。
ここでは、両方のヘッドが適用されるため、システムは決定論を判断できません。ただし、 >のゴールplus(X, s^n, s^m)には解がないことがわかっています。したがって、 のモデルを検討することで、選択ポイントをさらに回避できます。この休憩の後、すぐに戻ります。nmplus/3
call_semidet/1 を使用することをお勧めします!
ますます複雑になり、最適化によってプログラムに新しいエラーが簡単に導入される可能性があります。また、最適化されたプログラムを維持するのは悪夢です。実際のプログラミング目的では、むしろを使用しますcall_semidet/1。これは安全であり、仮定が間違っていることが判明した場合に明確なエラーが生成されます。
本題に戻ります: ここでさらに最適化を行います。Yとが同一の場合Z、2 番目の節は適用できません。
pluso2(X、Y、Z) :-
% パート 1: グリーン カット
( X == 0 -> ! % 最初の引数のインデックス付け
; Z == 0 -> ! % 第 3 引数の索引付け。例: Jekejeke、ECLiPSe
; Y == Z、地面(Z) -> !
; 真実
)、
% パート 2: 元の統合
X = 0、
Y = Z、
自然数(Z)。
pluso2(s(X), Y, s(Z)) :- pluso2(X, Y, Z).
私は（現在）pluso2/3、残りのチョイスポイントに関して、緑/青のカットの最適な使用法であると信じています. あなたは証拠を求めました。まあ、それはSOの答えをはるかに超えていると思います...
ground(Z)非終端性を確保するためにはゴールが必要です。ゴールplus(s(_), Z, Z)は終了しません。そのプロパティは によって保持されground(Z)ます。たぶん、無限の失敗ブランチも削除するのは良い考えだと思いますか? 私の経験では、これはかなり問題があります。特に、それらのブランチが自動的に削除される場合。一見、これは良いアイデアのように思えますが、プログラム開発をより脆くします: さもなければ無害なプログラム変更が最適化を無効にし、非終了を「引き起こす」可能性があります。とにかく、ここに行きます：
シンプルなグリーンカットを超えて
pluso3(X、Y、Z) :-
% パート 1: グリーン カット
( X == 0 -> ! % 最初の引数のインデックス付け
; Z == 0 -> ! % 第 3 引数の索引付け。例: Jekejeke、ECLiPSe
; Y == Z -> !
; var(Z), nonvar(Y), \+ unify_with_occurs_check(Z, Y) -> !, 失敗
; var(Z), nonvar(X), \+ unify_with_occurs_check(Z, X) -> !, 失敗
; 真実
)、
% パート 2: 元の統合
X = 0、
Y = Z、
自然数(Z)。
pluso3(s(X), Y, s(Z)) :- pluso3(X, Y, Z).
pluso3/3有限個の答えがあるのに が終わらない場合を見つけることができますか?