使用不纯原语的Prolog谓词的纯度 [英] Purity of Prolog predicates that use impure primitives

问题描述

我知道var/1，nonvar/1和!/0是不纯的基元，但是它们的使用是否会使使用它们的每个程序不纯?

I know that var/1, nonvar/1 and !/0 are impure primitives, but does their use make every program that uses them impure?

我写了下面的谓词plus/3，它的行为就像是纯的，或者至少是我所声称的.谓词是说明性的，并非旨在提高效率.

I wrote the following predicate plus/3 that behaves as if it were pure or at least that is what I claim. The predicate is demonstrative, not designed to be efficient.

% 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).

我有两个问题:

1. 上面的谓词plus/3真的是纯文本吗?
2. 通常，您如何证明特定关系具有逻辑纯性?

1. Is the above predicate plus/3 really pure?
2. In general, how can you prove that a particular relation has logical purity?

---

这个问题是关于答案的讨论之后的.

---

This question follows the discussion on this answer.

推荐答案

1. 上面的谓词plus/3真的很纯吗?

它有一些奇怪的行为:有时它接受算术表达式，有时不接受；尽管所有参数都被求值，但这是这样的:

It has some odd behavior: Sometimes it accepts arithmetic expressions, and sometimes not ; and this although all arguments are evaluated:

?- 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的效率低下:

I would rather be concerned about the inefficiency of nat/1 for cases like:

?- 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 ...

所以，在我看来，您的定义是纯正的.但是，这种编程风格使得很难保证此属性.最小的更改将带来灾难性的后果.

So, it looks to me that your definition is pure. However, this very style of programming makes it quite difficult to guarantee this property. A minimal change will have disastrous effects.

1. 通常，您如何证明特定关系具有逻辑纯性?

最简单的方法是通过构造.也就是说，仅使用纯单调构建基块.即，Prolog没有任何内置功能，仅使用常规目标的结合和分离.以这种方式构建的任何程序也将是纯净的和单调的. 然后，将Prolog标志发生检查设置为true或error.执行该程序.

The easiest way is by construction. That is, by using only pure monotonic building blocks. I.e., Prolog without any built-ins and using only conjunction and disjunction of regular goals. Any program built this manner will be pure and monotonic, too. Then, execute this program with Prolog flag occurs check set to true or error.

添加到像(=)/2和dif/2这样的纯内置函数中.

Add to this pure built-ins like (=)/2 and dif/2.

添加到此内置程序中，它们尝试模拟纯关系，并且在无法这样做时会生成实例化错误.考虑(is)/2和算术比较谓词.其中有些像call/N一样处于临界点，可能称为不纯谓词.

Add to this built-ins that try to emulate pure relations and that produce instantiation errors when they are unable to do so. Think of (is)/2 and the arithmetic comparison predicates. Some of these are quite on the borderline like call/N which might call some impure predicates.

添加带有标记 clpfd_monotonic 设置为true.

对于某些用途，许多构造是好的和纯净的，但对于其他用途则是不纯的.考虑一下if-then-else，它最适合进行算术比较:

Many constructs are fine and pure for certain uses, but impure for others. Think of if-then-else which is perfect for arithmetic comparison:

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

但不能与像这样的纯粹目标一起使用

but which does not work together with a pure goal like

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

剩下的是不纯净的内建函数，可用于构造纯行为的谓词；但其定义已不再是纯粹的.

What remains are impure built-ins that can be used to construct predicates that behave in a pure manner ; but whose definition as such is no longer pure.

例如，考虑真正的绿色削减.这些极为罕见，甚至在SO上也更为罕见.参见此和

As an example, consider truly green cuts. These are extremely rare, and even rarer here on SO. See this and that.

另一个提供纯关系的常见模式是条件，例如:

Another common pattern to provide a pure relation are conditionals like:

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

为防止未明确说明的情况，可能会引发错误.

And to guard against cases that are not cleanly covered, errors can be thrown.

这篇关于使用不纯原语的Prolog谓词的纯度的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！