I am reading the paper Implementing Type Theory in Higher Order Constraint Logic Programming, and on p7 I see the following lambda-prolog code:
% 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.
I am confused about the position of the cut ! in the third clause. My understanding of a cut is that it always succeeds, but prevents backtracking past that success, and in particular causes subsequent clauses for the same predicate to be ignored. In particular, a cut that comes first in a clause should mean that as soon as head unification with that clause succeeds, all later clauses are ignored.
With this in mind, the cuts that begin the first and second clauses above make sense to me: they say that if the term being reduced is an app or a lam, then only one rule can apply to it. But it looks to me as though the head of the third clause is fully general -- all the arguments are distinct variables -- so it can't fail to unify. Therefore, it seems to me that the cut that begins the third clause would always be invoked, and therefore the fourth clause would never be reached. I would have expected the third clause to be written something like
whd1 X S Ks Kf :- val X _ N NF, !, if (var NF) (whd_unwind N NF), Ks [] NF S.
so that it would apply only to what they call "val-bound variables"; the cut would then indicate that if X is such a variable, only this clause applies, while if X isn't such a variable then we would be able to backtrack and try the fourth clause.
However, my understanding of cut is very rudimentary, so I expect I am missing something. Can someone explain?
