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

问题描述

我知道 var/1、nonvar/1 和 !/0 是不纯的原语，但它们的使用会使 每个使用它们的程序都不纯?

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

% nat(X) 如果 X 是自然数则为真nat(0).nat(X):- nonvar(X), !, X >0.nat(X):- nat(X1)，X 是 X1 + 1.% plus(A, B, C) 如果 A,B 和 C 是自然数并且 A+B=C 则为真加(A，B，C):-nat(A),(nonvar(C), C < A, !, false ; true),加_(B，A，C).加_(A，B，C):-nat(A),(nonvar(C), C < A, !, false ; true),C1 是 A + B，(C = C1 ; nonvar(C), C 

我有两个问题:

1. 上面的谓词plus/3真的是纯的吗?
2. 一般而言，您如何证明特定关系具有逻辑纯度?

<小时>

此问题遵循关于此答案的讨论.

解决方案

1. 上面的谓词加/3真的是纯的吗?

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

?- plus(3,5-3,5).真的 ...?- 加(3,2,3+2).错误的.?- 加(3,2,3+b).错误:</2:算术:b/0"不是函数?- 加(3,2,3+Z).错误:</2:参数没有充分实例化

我宁愿担心 nat/1 在以下情况下效率低下:

?- time(( nat(X), X > 9999 ) ).% 50,025,002 推理，27.004 CPU 在 27.107 秒内(100% CPU，1852480 唇)X = 10000 ;% 10,006 次推理，0.015 秒内 0.015 CPU(99% CPU，650837 唇)X = 10001 ;% 10,005 次推理，0.016 秒内 0.016 CPU(99% CPU，631190 唇)X = 10002 ...

所以，在我看来，您的定义是纯粹的.然而，这种编程风格很难保证这个属性.一个微小的改变就会产生灾难性的影响.

<块引用>

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

最简单的方法是通过构建.也就是说，仅使用纯单调构建块.即，Prolog 没有任何内置函数，仅使用常规目标的合取和析取.以这种方式构建的任何程序也将是纯粹且单调的.然后，执行这个程序，将 Prolog 标志发生检查设置为 true 或 error.

添加到这个纯内置函数中，例如 (=)/2 和 dif/2.

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

添加带有 clpfd_monotonic 设置为 true.

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

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

但它不能与像这样的纯粹目标一起工作

 ..., ( X = Y -> ... ; ... ), ... % 不纯

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

例如，考虑真正的绿色切割.这些非常罕见，在 SO 上甚至更罕见.请参阅 this 和 那个.

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

..., ( var(V) -> 带有 var 的东西；等价于 nonvar ), ...

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

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

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

I have two questions:

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. Is the above predicate plus/3 really pure?

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

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.

2. In general, how can you prove that a particular relation has logical purity?

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.

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

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.

Add library(clpfd) with flag clpfd_monotonic set to true.

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.

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屋！