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

我有两个问题:

1. 上面的谓词plus/3真的很纯粹吗？
2. 一般来说,如何证明特定关系具有逻辑纯度？

---

这个问题跟随对这个答案的讨论.

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没有任何内置插件,仅使用常规目标的连接和分离.以这种方式构建的任何程序也将是纯粹和单调的.然后,执行此程序与Prolog标志发生检查设置为true或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 ), ...

为防止未完全覆盖的案例,可能会引发错误.

Answer 2

关于"上面plus/3真的是纯粹的吗？" 这个问题.我只能说:我不知道这里保留了哪些属性,因为由于所有这些超逻辑谓词,代码是如此复杂且难以理解,因此很难说它实际上在做什么.我真的必须说在这种情况下做,因为这远远不是描述我们可以比较容易谈论的东西的声明性代码.在这种情况下,我们期望从声明性代码中获得的各种属性可能会被破坏.

通常证明关系纯粹的最好方法是将自己限制在Prolog 的纯粹和单调子集中.出于这个原因,这个属性非常重要,因为这个子集在组合下是封闭的.一旦你离开这个子集,很快就很难证明你的程序的任何属性,正如你的例子很好地演示.

例如,为了证明你的plus/3单调性,你需要在许多其他事情中表明,如果任何一个术语?- plus(X, _, _), X = T 失败T,那么?- X = T, plus(X, _, _)就不会成功.由于查询失败,循环或成功通常是不可判定的,因此我们通常甚至无法确定这一含义的单方面,更不用说两者,我只能说:祝你好运!