6

次のルールがあります

% Signature: natural_number(N)/1
% Purpose: N is a natural number.
natural_number(0).
natural_number(s(X)) :-
   natural_number(X).

ackermann(0, N, s(N)). % rule 1
ackermann(s(M),0,Result):-
   ackermann(M,s(0),Result). % rule 2
ackermann(s(M),s(N),Result):-
   ackermann(M,Result1,Result),
   ackermann(s(M),N,Result1). % rule 3

クエリは次のとおりackermann (M,N,s(s(0)))です。

さて、私が理解したように、3番目の計算では、無限の検索(失敗ブランチ)が得られました。確認したところ、有限検索(失敗分岐)が出ました。

説明します:最初に、M = 0、N = s(0)の置換を取得しました(ルール1-成功!)。2番目では、M = s(0)、N = 0の置換を取得しました(ルール2-成功!)。しかし、今は何ですか?M = s(s(0))N = 0に一致させようとしましたが、有限検索-失敗ブランチが得られました。コンパイラが私に「失敗」と書かないのはなぜですか。

ありがとうございました。

4

2 に答える 2

8

トムがここで何を求めているのかを正確に理解するのは少し難しかったです。おそらく、述語natural_number/1が何らかの形でackermann /3の実行に影響を与えるという予想があります。ならない。後者の述語は純粋に再帰的であり、 natural_number/1に依存するサブゴールを作成しません。

示されている3つの節がackermann/3に対して定義されている場合、目標は次のとおりです。

?- ackermann(M,N,s(s(0))).

SWI-Prologは、トムが報告する2つのソリューションを(バックトラックを使用して)検出し、無限再帰になります(「スタック外」エラーが発生します)。この無限再帰には、ackermann / 3に与えられた3番目の節(コード内のTomのコメントごとのルール3)が含まれていると確信できます。

M = 0,
N = s(0) ;
M = s(0),
N = 0 ;
false.

トムは、送信されたクエリを、有限検索(1つのソリューションを見つけてバックトラックに失敗する)を設定し、生成するクエリに変更すると、前のクエリによって生成された無限再帰と一致する理由の説明を求めているようです。ここでの私の疑いは、Prologエンジンが(元のクエリに対して)バックトラックで何を試みるかについて誤解があるということです。そこで、それを掘り下げていきます。うまくいけば、それはトムの問題を解決しますが、それが解決するかどうか見てみましょう。確かに私の扱いは言葉遣いですが、Prolog実行メカニズム(サブゴールの統一と解決)は研究する価値があります。M = s(s(0))N = 0

[追加: 述語は、完全に計算可能ですが原始再帰ではない有名なアッカーマン関数との明らかな関係があります。この関数は急速に成長することが知られているため、非常に大きいが有限の再帰も可能であるため、無限の再帰を要求する場合は注意が必要です。ただし、3番目の句は、2つの再帰呼び出しを、私が行ったのとは逆の順序で配置します。この反転は、以下のコードをステップ実行するときに見つかる無限再帰で重要な役割を果たしているようです。]

トップレベルの目標ackermann(M,N,s(s(0)))が提出されると、SWI-Prologは、与えられたクエリと「頭」が一致するものが見つかるまで、 ackermann / 3に対して定義された句(ファクトまたはルール)を試行します。Prologエンジンは、最初の節、この事実として遠くを見る必要はありません:

ackermann(0, N, s(N)).

統一し、拘束M = 0N = s(0)、最初の成功としてすでに説明したように。

ユーザーがセミコロンを入力するなどしてバックトラックを要求された場合、Prologエンジンは、この最初の句を満たす別の方法があるかどうかを確認します。存在しない。次に、Prologエンジンは、指定された順序でackermann/3に対して次の句を試行します。

この場合も、2番目の句の先頭もクエリと統合されるため、検索を遠くまで行う必要はありません。この場合、次のルールがあります。

ackermann(s(M),0,Result) :- ackermann(M,s(0),Result).

クエリとこのルールの先頭を統合すると、クエリで使用される変数に関してバインディングM = s(0)が生成されます。上記のルールで使用される変数に関して、および。統合は、呼び出し引数としての外観によって用語と一致し、クエリ/ルールの境界を越えて再利用される変数名をIDを示すものとは見なさないことに注意してください。N = 0M = 0Result = s(s(0))

この節は(頭だけでなく体も持つ)規則であるため、統一はそれを成功させるための最初のステップにすぎません。Prologエンジンは、このルールの本文に表示される1つのサブゴールを試行します。

ackermann(0,s(0),s(s(0))).

このサブゴールは、ルールで使用されている「ローカル」変数を統一の値、M = 0およびに置き換えることで得られることに注意してくださいResult = s(s(0))。Prologエンジンは、このサブゴールが満たされるかどうかを確認するために、述語ackermann/3を再帰的に呼び出しています。

ackermann / 3の最初の節(事実)が明白な方法で統合されるように(実際、節で使用される変数に関しては以前と本質的に同じ方法で)可能です。したがって(この再帰呼び出しが成功すると)、2番目のソリューションが外部呼び出し(最上位のクエリ)で成功します。

ユーザーがPrologエンジンにもう一度バックトラックするように要求すると、現在の句(ackermann / 3の2番目の句)が別の方法で満たされるかどうかを再度確認します。それはできないので、検索は述語ackermann / 3の3番目(そして最後)の節に渡して続行されます。

ackermann(s(M),s(N),Result) :-
    ackermann(M,Result1,Result),
    ackermann(s(M),N,Result1).

この試みは無限の再帰を生成することを説明しようとしています。トップレベルのクエリをこの句の先頭と統合すると、クエリ内の用語を先頭の用語と揃えることでおそらく明確に理解できる引数のバインディングが得られます。

   query     head
     M       s(M)
     N       s(N)
   s(s(0))  Result

ルール内の変数と同じ名前のクエリ内の変数は統合を制約しないことを念頭に置いて、この3つの用語を統合することができます。クエリMはheadになります。これは、headに表示されるまだ不明な変数に適用されるs(M)ファンクターを含む複合用語です。クエリについても同じです。これまでのところ、唯一の「グラウンド」用語は、クエリからバインドされているルールのヘッド(および本体)に表示される変数です。sMNResults(s(0))

現在、3番目の節はルールであるため、Prologエンジンは、そのルールの本体に表示されるサブゴールを満たそうとして続行する必要があります。頭の統一から体に値を代入する場合、満たす最初のサブゴールは次のとおりです。

ackermann(M,Result1,s(s(0))).

Resultここでは、統合でバインドされた値に置き換えたことを除いて、句の「ローカル」変数を使用したことを指摘しておきます。ここNで、元の最上位クエリを変数名Result1に置き換えることを除けば、このサブゴールの元のクエリと同じことを要求していることに注意してください。確かに、それは私たちが無限再帰に入ろうとしているかもしれない大きな手がかりです。

ただし、それ以上の解決策が報告されない理由を確認するには、もう少し議論が必要です。これは、その最初のサブゴールの最初の成功は(前に見つけたように)andを必要M = 0Result1 = s(0)し、Prologエンジンは次に節の2番目のサブゴールを試みるために進む必要があるためです。

ackermann(s(0),N,s(0)).

残念ながら、この新しいサブゴールは、ackermann / 3の最初の節(ファクト)と統合されていません。次のように、2番目の句の先頭と統合されます

   subgoal     head
     s(0)      s(M)
      N         0
     s(0)     Result

しかし、これは(2番目の節の本文からの)サブサブゴールにつながります:

ackermann(0,s(0),s(0)).

これは、最初の節または2番目の節のどちらの先頭とも一致しません。また、3番目の句の先頭と統合されません(最初の引数の形式が必要s(_)です)。そのため、検索ツリーで単一障害点に到達しました。Prologエンジンは、3番目の節の本体の最初のサブゴールが別の方法で満たされるかどうかを確認するためにバックトラックするようになりました。私たちが知っているように、それは可能です(このサブゴールは基本的に元のクエリと同じであるため)。

M = s(0)、そしてResult1 = 0その2番目の解決策は、3番目の節の本体の2番目のサブゴールのためにこれにつながります:

ackermann(s(s(0)),N,0).

これは述語の最初の節(ファクト)と統合されませんが、2番目の節の先頭と統合されます。

   subgoal     head
   s(s(0))     s(M)
      N         0
      0       Result

しかし、成功するためには、Prologエンジンは2番目の節の本体も満たす必要があります。

ackermann(s(s(0)),s(0),0).

これは、 ackermann/3の最初または2番目の節の先頭と統合できないことが簡単にわかります。これは、3番目の節の先頭と統合できます。

  sub-subgoal  head(3rd clause)
    s(s(0))       s(M)
      s(0)        s(N)
       0         Result

今ではおなじみのように、Prologエンジンは、3番目の節の本体の最初のサブゴールが満たされるかどうかを確認します。これはこのサブサブサブゴールに相当します。

ackermann(s(0),Result1,0).

これは、最初の節(fact)との統合に失敗しますが、2番目の節の先頭との結合を結合しM = 0、(使い慣れたロジックによって)sub-sub-sub-subgoalを生成します。Result1 = 0Result = 0

ackermann(0,0,0).

これは3つの節の頭のいずれとも統一できないため、これは失敗します。この時点で、Prologエンジンは、3番目の節を使用して上記のサブサブサブゴールを満たそうとすることに戻ります。統合は次のようになります。

  sub-sub-subgoal  head(3rd clause)
       s(0)             s(M)
      Result1           s(N)
         0             Result

そして、Prologエンジンのタスクは、3番目の節の本体の最初の部分から派生したこのサブサブサブサブゴールを満たすことです。

ackermann(0,Result1,0).

しかし、これは3つの条項のいずれの先頭とも一致しません。上記のサブサブサブゴールの解決策の検索は失敗に終わります。Prologエンジンは、元のトップレベルクエリによって呼び出された3番目の句の2番目のサブゴールを最初に満たそうとしたところまでバックトラックします。これは、現在失敗しているためです。言い換えると、3番目の節の最初のサブゴールの最初の2つのソリューションでそれを満たそうとしました。これは、元のクエリと変数名の変更を除いて、本質的に同じでした。

ackermann(M,Result1,s(s(0))).

上で見たのは、ackermann / 3の最初と2番目の節から元のクエリを複製するこのサブゴールのソリューションでは、3番目の節の本体の2番目のサブゴールが成功しないことです。したがって、Prologエンジンは、3番目の節を満たすソリューションを見つけようとします。しかし、明らかにこれは無限再帰になります。これは、その3番目の句が頭の中で統一されるためですが、3番目の句の本体は、先ほど追跡したのとまったく同じ検索を繰り返します。そのため、Prologエンジンは、3番目の節の本体に際限なく入り込むことになります。

于 2011-06-26T00:55:23.380 に答える
5

質問を言い換えると、クエリackermann(M,N,s(s(0))).は2つのソリューションを見つけて、ループします。理想的には、他に存在せず、値がであるため、これら2つのソリューションの後で終了NMますs(s(0))

では、なぜクエリが普遍的に終了しないのでしょうか。これを理解することは非常に複雑になる可能性があり、最善のアドバイスは、正確な実行メカニズムを理解しようとしないことです。非常に単純な理由があります。Prologの実行メカニズムは非常に複雑であるため、コードをステップスルーして理解しようとすると、とにかく誤解されやすくなります。

false代わりに、次のことを試すことができます。プログラムの任意の場所に目標を挿入します。結果のプログラムが終了しない場合、元のプログラムも終了しません。

あなたの場合:

ackermann(0、N、s(N)):- falseackermann(s(M)、0、Result):- falseackermann(M、s(0)、Result)。
ackermann(s(M)、s(N)、Result):-
   ackermann(M、Result1、Result)、false、
    ackermann (s(M)、N、Result1)

これで、最初と2番目の句を削除できます。そして3番目の節では、falseの後にゴールを削除できます。したがって、次のフラグメントが終了しない場合、元のプログラムも終了しません。

ackermann(s(M),s(N),Result):-ackermann(M,Result1,Result), false.

このプログラムは、最初の引数がわかっている場合にのみ終了するようになりました。しかし、私たちの場合、それは無料です...

つまり、プログラムのごく一部(と呼ばれる)を検討することで、プログラム全体のプロパティをすでに推測することができました。詳細については、この論文およびサイトの他の論文を参照してください。

残念ながら、この種の推論は、終了しない場合にのみ機能します。終了については、物事はより複雑です。最良の方法は、終了条件を推測し、それらの最適性を証明しようとするcTIのようなツールを試すことです。私はすでにあなたのプログラムに入ったので、もし修正して効果を見てみてください!

この小さなフラグメントは、2番目の引数が終了1に影響を与えないことも示しています。つまり、のようなクエリackermann(s(s(0)),s(s(0)),R).も終了しません。目標を交換して違いを確認してください...


1正確には、と統一されない用語はs(_)終了に影響します。考えてみてください0。ただし、、、s(0)...s(s(0))は終了に影響しません。

于 2011-06-24T19:18:22.547 に答える