我正在阅读在高阶约束逻辑编程中实现类型理论的论文，在 p7 上我看到了以下 lambda-prolog 代码：
% KAM-like rules in CPS style
whd1 (app M N) S Ks Kf :- !, Ks [] M [N|S].
whd1 (lam T F1) [N|NS] Ks Kf :- !, pi x \ val x T N NF => Ks [x] (F1 x) NS.
whd1 X S Ks Kf :- !, val X _ N NF, if (var NF) (whd_unwind N NF), Ks [] NF S.
whd1 X S Ks Kf :- Kf.
!我对第三条中cut的位置感到困惑。我对 cut 的理解是它总是成功的，但会阻止回溯到该成功之后，特别是会导致同一谓词的后续子句被忽略。特别是，在子句中首先出现的剪切应该意味着一旦与该子句的头部统一成功，所有后面的子句都将被忽略。
考虑到这一点，上面第一条和第二条开始的削减对我来说是有意义的：他们说如果被归约的术语是 anapp或 a lam，那么只有一个规则可以适用于它。但在我看来，第三个子句的开头似乎是完全一般的——所有的论点都是不同的变量——所以它不能不统一。因此，在我看来，总是会调用从第三个子句开始的剪切，因此永远不会到达第四个子句。我本来希望第三个子句写成类似
whd1 X S Ks Kf :- val X _ N NF, !, if (var NF) (whd_unwind N NF), Ks [] NF S.
所以它只适用于他们所谓的“val-bound variables”；然后剪切将指示 ifX是这样一个变量，只有这个子句适用，而 if Xis not such a variable 那么我们将能够回溯并尝试第四个子句。
但是，我对 cut 的理解非常初级，所以我希望我遗漏了一些东西。有人可以解释吗？