8

とが不純なプリミティブであることは知っていますが、それらを使用すると、それらを使用するvar/1すべてのプログラムが不純になりますか?nonvar/1!/0

plus/3私は、あたかも純粋であるかのように振る舞う次の述語を書きました。述語は実証的であり、効率的に設計されていません。

% nat(X) is true if X is a natural number

nat(0).
nat(X):- nonvar(X), !, X > 0.
nat(X):- nat(X1), X is X1 + 1.

% plus(A, B, C) is true if A,B and C are natural numbers and A+B=C

plus(A, B, C):-
    nat(A),
    (nonvar(C), C < A, !, false ; true),
    plus_(B, A, C).

plus_(A, B, C):-
    nat(A),
    (nonvar(C), C < A, !, false ; true),
    C1 is A + B,
    (C = C1 ; nonvar(C), C < C1, !, false).

2 つの質問があります。

  1. 上記の述語plus/3は本当に純粋ですか?
  2. 一般に、特定の関係が論理的に純粋であることをどのように証明できますか?

この質問は、この回答に関する議論に続きます。

4

2 に答える 2

7
  1. 上記の述語 plus/3 は本当に純粋ですか?

いくつかの奇妙な動作があります。算術式を受け入れる場合と受け入れない場合があります。これは、すべての引数が評価されますが、次のとおりです。

?- plus(3,5-3,5).
true ...

?- plus(3,2,3+2).
false.

?- plus(3,2,3+b).
ERROR: </2: Arithmetic: `b/0' is not a function

?- plus(3,2,3+Z).
ERROR: </2: Arguments are not sufficiently instantiated

nat/1次のような場合の非効率性について心配したいと思います。

?- time( ( nat(X), X > 9999 ) ).
% 50,025,002 inferences, 27.004 CPU in 27.107 seconds (100% CPU, 1852480 Lips)
X = 10000 ;
% 10,006 inferences, 0.015 CPU in 0.015 seconds (99% CPU, 650837 Lips)
X = 10001 ;
% 10,005 inferences, 0.016 CPU in 0.016 seconds (99% CPU, 631190 Lips)
X = 10002 ...

だから、あなたの定義は純粋に見えます。ただし、このスタイルのプログラミングは、このプロパティを保証することを非常に困難にします。最小限の変更で悲惨な結果が生じます。

  1. 一般に、特定の関係が論理的に純粋であることをどのように証明できますか?

最も簡単な方法は、建設によるものです。つまり、純粋に単調なビルディング ブロックのみを使用します。つまり、ビルトインを使用せず、通常のゴールの結合と分離のみを使用する Prolog です。この方法で構築されたプログラムも、純粋で単調になります。次に、Prolog フラグ発生チェックをtrueまたはに設定して、このプログラムを実行しerrorます。

この純粋なビルトインに と を追加し(=)/2ますdif/2。

純粋なリレーションをエミュレートしようとし、それができない場合にインスタンス化エラーを生成する組み込み関数を追加します。(is)/2および算術比較述語を考えてみてください。これらのいくつかは、境界線上にあり、call/N不純な述語と呼ばれる可能性があります。

library(clpfd)フラグclpfd_monotonicを に設定して追加しtrueます。

多くのコンストラクトは、特定の用途では問題なく純粋ですが、他の用途では不純です。算術比較に最適な if-then-else を考えてみましょう。

 ..., ( X > Y -> ... ; ... ), ...

しかし、これは次のような純粋な目標とは連携しません

 ..., ( X = Y -> ... ; ... ), ...  % impure

残っているのは、純粋な方法で動作する述語を構築するために使用できる不純な組み込みです。しかし、その定義自体はもはや純粋ではありません。

例として、真にグリーンなカットを考えてみましょう。これらは非常にまれであり、ここ SO ではさらにまれです。あれこれ見て。_

純粋な関係を提供するもう 1 つの一般的なパターンは、次のような条件です。

..., ( var(V) -> something with var ; the equivalent with nonvar ), ...

また、完全にカバーされていないケースを防ぐために、エラーをスローすることができます。

于 2015-01-13T15:10:26.663 に答える