4

私は半決定論的な機能を持っています。if ステートメントの代わりにパターン マッチングを使用するように書き直すと、Mercury は非決定論的になると言います。理由が知りたいです。

元のコード:

:- pred nth(list(T), int, T).
:- mode nth(in,      in,  out) is semidet.
nth([Hd | Tl], N, X) :- (if N = 0 then X = Hd else nth(Tl, N - 1, X)).

改訂されたコード:

:- pred nth(list(T), int, T).
:- mode nth(in,      in,  out) is nondet.
nth([Hd | _], 0, Hd).                             % Case A
nth([_ | Tl], N, X) :- N \= 0, nth(Tl, N - 1, X). % Case B

私は、SML でのパターン マッチングについて考えるのに慣れています。A の場合の 0 は、B の場合の N が 0 でないことを保証します。Mercury の動作は異なりますか? N が 0 の場合でも、ケース B が呼び出される可能性はありますか? N \= 0(述語を半決定論的にするためにケース B に節を追加しましたが、うまくいきませんでした。)

半決定論的でもあるパターンマッチングでこの述語を書く方法はありますか?

4

1 に答える 1

8

はい、MercuryパターンマッチングはSMLとは動作が異なります。Mercuryは、その宣言型セマンティクスについてかなり厳密です。複数の節を持つ述語は、すべての本体の論理和に相当し（節の頭の統一のためのいくつかの複雑さを法として）、論理和の意味は、論理和のさまざまなアームが書かれる順序に影響されません。実際、Mercuryのほとんどは、あなたが物事を書く順序によって影響を受ける意味を持っていません（状態変数は私が考えることができる唯一の例です）。

したがってN \= 0、本文を挿入しないと、パターンマッチングを使用した2つの句を含む述語は非決定的です。nth(Tl, 0 - 1, X)の有効な削減であることを止めるものは何もありませんnth([_ | Tl], 0, X)。

を使用するN \= 0と、正しい方向に進んでいます。残念ながら、論理的if A then B else Cにはと同等ですが、Mercuryの決定論的推論は、通常、その逆を理解するのに十分なほど賢くはありません。(A, B) ; (not A, C)

特に、Mercuryの決定論的推論は、2つの節が相互に排他的であることを一般的に理解しようとはしていません。この場合、N = 0の値に応じて成功または失敗する可能性があり、の値に応じて成功または失敗する可能性がNあることを認識N \= 0していますN。述語が成功するための2つの異なる方法があり、失敗する可能性があるため、非決定論的である必要があります。コンパイラーに、決定論が推測されるものではないことを約束する方法がありますが、このような場合は、if / then/elseを使用することに固執する方が簡単です。

コンパイラーが複数のソリューションを使用できると考えずにパターンマッチングを使用できる場合は、1つの変数を同じタイプの複数の異なるコンストラクターと照合する場合です。例えば：

:- pred some_pred(list[T]) is det.
some_pred([]) :- something.
some_pred([H | T]) :- something_else.

これはスイッチと呼ばれます。コンパイラーは、リストに2つのコンストラクター（空のリスト[]またはconsセル[|]）があり、指定されたリストはそのうちの1つにしかできないことを認識しているため、両方のコンストラクターのアームを持つ論理和（または述語の複数の節）が必要です。決定論的であること。すべてではないが一部のコンストラクターのケースを含む論理和（複数の節）は、半決定論的であると推測されます。

Mercuryは、スイッチの非常に効率的なコードを生成することもできます。また、新しいケースを追加してタイプを変更すると、変更が必要なすべての場所を通知するため、可能な場合はスイッチを使用することをお勧めします。ただし、あなたのような場合は、if / then/elseで立ち往生しています。

于 2011-09-19T06:37:44.590 に答える