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

我有两个问题：

  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 没有任何内置函数，仅使用常规目标的合取和析取。以这种方式构建的任何程序也将是纯粹且单调的。true然后，在 Prolog 标志发生检查设置为或的情况下执行该程序error。

添加到这个纯粹的内置插件，如(=)/2和dif/2。

添加到这个试图模拟纯关系并在它们无法这样做时产生实例化错误的内置函数。想想(is)/2和算术比较谓词。其中一些非常接近边界call/N，可能称为一些不纯谓词。

添加library(clpfd)标志clpfd_monotonic设置为true.

许多构造对于某些用途来说是好的和纯粹的，但对于其他用途来说是不纯的。想想 if-then-else，它非常适合算术比较：

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

但它不能与一个纯粹的目标一起工作，比如

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

剩下的是不纯的内置函数，可用于构造以纯方式表现的谓词；但其定义本身不再是纯粹的。

例如，考虑真正的绿色切割。这些非常罕见，在 SO 上甚至更罕见。看到这个那个。_

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

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

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

于 2015-01-13T15:10:26.663 回答
6

关于“以上plus/3真的是纯的吗？”这个问题。我只能说：我不知道这里保留了哪些属性，因为由于所有这些额外的逻辑谓词，代码是如此复杂且难以理解，以至于很难说出它实际上在做什么。我真的必须说在这种情况下做，因为这与描述我们可以相对容易谈论的东西的声明性代码相去甚远。在这种情况下，我们期望从声明性代码中获得的所有类型的属性都可能被破坏。

通常证明一个关系是纯的最好的方法是将自己限制在 Prolog的纯单调子集。正是由于这个原因，这个属性如此重要，因为这个子集在合成下是封闭的。一旦你离开这个子集，很快就很难证明你的程序的任何属性，正如你的例子很好地展示的那样。

例如，为了证明你的plus/3单调性，你需要证明，如果任何一项都?- plus(X, _, _), X = T 失败T，那么?- X = T, plus(X, _, _)就不会成功。由于通常无法确定查询是失败、循环还是成功，因此我们通常甚至无法确定这种含义的单一方面，更不用说两者了，我只能说：祝你好运！

于 2015-01-12T20:23:28.813 回答