prolog - 使用不纯原语的 Prolog 谓词的纯度

Question

我知道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).

我有两个问题:

是上面的谓词plus/3真的纯吗？

一般而言，您如何证明特定关系具有逻辑纯度？

这个问题跟在这个 answer的讨论之后.

Answer 1

1. Is the above predicate plus/3 really pure?

它有一些奇怪的行为:有时它接受算术表达式，有时不接受；这虽然所有参数都被评估:

?- 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. In general, how can you prove that a particular relation has logical purity?

最简单的方法是通过构建。也就是说，只使用纯单调的构建块。即，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 上甚至更罕见。见 this和 that .

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

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

为了防止没有完全覆盖的情况，可能会抛出错误。