我是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):- !.
我现在想知道这是否是正确的方法。目前它似乎有效，但我想知道这在某些边缘情况下是否不符合我所期望的属性，我写它的方式是否存在一些性能问题，或者这只是糟糕的编码风格/实践。
使用剪切时会出现几个问题。
你在写什么样的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(S, R):- var(S), !, ...中的normal/2中，剪切确保所有后续子句只考虑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
伤口来的太晚了。