1

我是 Prolog 和一般逻辑编程的新手，我正在编写一个小定理证明器来取乐，并在这样做的过程中编写了一个规范化程序。我希望这个过程是确定性和坚定的，所以我写了这样的东西：

normal(S, R):- var(S), !, S = R.
normal(true(S), R):- !, normal(S, R).
normal(!(S), R):- !, normal(false(S), R).
normal(P => Q, R):- !, normal(false(P and false(Q)), R).
normal(A or B, R):- !, normal(false(false(A) and false(B)), R).
normal(false(S), R):- !, normal(S, NS), normal_false(NS, R).
normal(A and B, R):- !, normal(A, NA), normal(B, NB), normal_and(NA, NB, R).
normal(S, S):- !.

normal_false(S, R):- var(S), !, S = false(R).
normal_false(false(S), S):- !.
normal_false(true, false):- !.
normal_false(false, true):- !.
normal_false(S, false(S)):- !.

normal_and(A, B, R):- var(A), var(B), !, R = A and B.
normal_and(A, true, A):- !.
normal_and(true, B, B):- !.
normal_and(_, false, false):- !.
normal_and(false, _, false):- !.
normal_and(A, B, A and B):- !.

我现在想知道这是否是正确的方法。它目前似乎可以工作，但我想知道这是否不符合我在某些极端情况下所期望的属性，我编写它的方式是否可能存在一些性能问题，或者这只是糟糕的编码风格/一般练习。

4

1 回答 1

4

使用剪辑时会出现几个问题。

你在写什么样的 Prolog 程序？

这里有几种可能性。从纯程序开始，仅考虑一组解决方案就可以以声明方式理解。在这样的程序中，有很多理想的属性，但你的显然不是其中之一。毕竟，目标normal_false(false, true)成功了，但它的泛化却normal_false(V, true)失败了（如预期的那样）。所以normal_false/2不是纯粹的关系。

您的程序将 Prolog 变量视为对象。它是一个元逻辑程序，这并不奇怪，因为您想通过重用 Prolog 的基础设施来实现证明者。在这里，仍然有许多不错的属性，例如，您可能仍然使用来确定未终止的原因。然而，使用var/1特别容易出错，因为 Prolog 无法枚举所有可能的解决方案，因此很容易忘记一两个案例。在您的示例中（在添加缺少的运算符声明之后）：

?- normal(X and true, N).
   X = N.                   % expected       
?- normal(true and X, N).
   X = true, N = true.      % unexpected

切掉的是什么？

在normal/2第一个子句中normal(S, R):- var(S), !, ...，cut 确保所有后续子句只考虑 case nonvar(S)。

normal(S, S):- !.如果论点统一，则可疑是最后一个删除的子句。乍一看，这并没有什么区别，因为它是最后一个子句。但是如果你会得到不同的结果，比如说freeze(S, ( T = 1 ; T = 2 ) )。但除此之外，normal/2似乎还可以。

更没有说服力的是削减normal_and/2。除了上述异常之外，这个定义也并不坚定。毕竟，结果受其最后一个论点的影响：

?- normal(true and true, N).
   N = true.      % expected
?- normal(true and true, true and true).
   true.          % unexpected

这里的削减来得太晚了。

于 2021-05-23T14:20:59.657 回答