Is it possible to express Prolog's cut in first order logic?

Question

In conversations around Prolog's cut operator !/0, I have only ever heard it described in terms of choice points and Prolog's execution model. It also seems to me that cut was introduced to give more "imperative" control over the search procedure, and to potentially improve the performance of some programs, but not so much for theoretical reasons. For examples of such discussions, see SWI Prolog's documentation, SICStus Prolog's documentation, and the Wikipedia article on cuts.

I'm curious if there are other ways of thinking about cuts in Prolog code? Specifically, can cut be given (possibly messy) declarative semantics in the language of first order logic? Second order logic? Higher order logic? If not, are there extensions to these logics that make it possible to implement cut?

Answer 1

"Purely for performance"?

Cuts are convenient, as a sometimes-more-elegant alternative to if-then-else.

Answer 2

There is no declarative semantics for the cut in the general case. It suffices to consider one counterexample:

?- X = 2, ( X = 1 ; X = 2 ), !.
   X = 2.
?-        ( X = 1 ; X = 2 ), !, X = 2.
   false.

So once it is the case and once not. Therefore, conjunction is not commutative. But to have a declarative semantics, conjunction must be commutative. And even in Pure Prolog commutativity of conjunction holds¹. So maybe there is some way to twist the meaning of declarative. But twisting it that far is just too much.

The only statement we can say is that in a program with cuts the search space is somehow pruned compared to the very same program without cuts. But usually that is not that interesting. Think of Prolog negation.

mynot(G_0) :-
   G_0,
   !,
   false.
mynot(_G_0).

So this is compared to its cut free version where the fact will always ensure success. The meaning of negation is therefore lost in the cut free program.

However, some uses of cuts do have a declarative semantics. But those cuts are typically guarded to ensure that it does not cut too often. These guards may come in different styles. One possibility is to produce an instantiation error in case the arguments are not sufficiently instantiated. Another is to fail and resort to the original definition. Another is to ensure that arguments are sufficiently instantiated by some mode system. As long as such mode system is actually enforced it is a declarative option. However, if modes are only commentary decorum, the declarative meaning is lost.

---

_{1 Conjunction in Pure Prolog is commutative modulo termination and errors.}