私は<code>var/1</code>、<code>nonvar/1</code>と<code>!/0</code>は不純なプリミティブであることを知っている

Question

不純なプリミティブを使用しPrologの述語の純度が、その使用は、彼らが不純使用すべてのプログラムを作るのですか？

私は次の述語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. 一般的に、特定の関係に論理的純度があることを証明するにはどうすればよいですか？

---

この質問は、このanswer上の議論に従います。

Answer 1

1. 上記の述語は/ 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 ... 

、それはあなたの定義が純粋であるように私には見えます。しかし、このようなプログラミングスタイルは、このプロパティを保証することを非常に困難にしています。最小限の変更は悲惨な影響を与えます。

一般に

<オール=「2」を起動>、どのように特定の関係が論理的純度を有することを証明することができますか？

最も簡単な方法は建設によるものです。つまり、純粋な単調なビルディングブロックのみを使用します。つまり、Prologは組み込み関数がなく、通常の目的との結合と不一致のみを使用します。この方法で構築されたプログラムは純粋で単調なものになります。 次に、またはerrorに設定されたPrologフラグの発生チェックでこのプログラムを実行します。

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

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

はtrueに設定されたフラグclpfd_monotonicとlibrary(clpfd)を追加します。

多くの構成要素は、ある用途では純粋で純粋ですが、他の構成要素には不都合です。算術比較のために完璧であるされたif-then-elseを考える：

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

が、使用することができます

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

遺骨が不純されているどのような組み込み関数のような純粋な目的と一緒に動作しません。純粋な振る舞いをする述語を構成する。しかしそのような定義はもはや純粋ではない。

例として、本当に緑色のカットを考えてみましょう。これらは非常にまれであり、ここではまれです。 thisおよびthatを参照してください。

純粋な関係を提供するために、他の一般的なパターンのような条件文です：

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

そしてきれいにカバーされていない場合を防ぐために、エラーがスローされることがあります。

Answer 2

質問については、上記のplus/3は本当に純粋ですか？私は言うことができます：どのようなプロパティがここに保存されているのか分かりません。これらの余分な論理的な述語のためにコードが複雑で難しいので、実際に何をしているのか分かりません。そして、これはの場合はとなります。なぜならこれはと書かれた宣言的なコードではありません。という比較的簡単に話すことができます。この場合、宣言型コードから期待されるあらゆる種類のプロパティが破棄される可能性があります。

一般的に関係が純粋であることを証明するための最良の方法は、プロローグの純粋と単調サブセットに自分自身を制限することです。この理由から、このサブセットは構成上閉じられているため、このプロパティは非常に重要です。このサブセットを離れると、あなたのプログラムがどのような性質を持つかを素早く証明することができます。

たとえば、証明するためにあなたのplus/3単調、あなたは?- plus(X, _, _), X = Tは、任意の用語Tためを失敗した場合、その後、?- X = T, plus(X, _, _)はを成功しないことを、他の多くのもののうち、表示する必要があり。クエリが失敗するかどうかは一般的に判断できないため、ループしたり成功したりするため、一般的にこの含意の片側を判断することすらできません。