2

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?

jweightman
  • 328
  • 1
  • 12
  • I'm not sure it's relevant... without cut, Prolog cannot express the negation. Guess this has to do with termination, since first order logic doesn't bother with infinity... – CapelliC Oct 07 '22 at 17:12
  • From the abstract *If the cut is used to implement functional predicates and if, furthermore, a certain discipline in its use is adhered to, then programs using the cut operator do possess a declarative semantics.* everyone agrees with that. – false Oct 07 '22 at 18:01

2 Answers2

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 holds1. 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.

false
  • 10,264
  • 13
  • 101
  • 209
  • 1
    Thanks for the thoughtful response. Are you aware of any semantics-preserving program transformations that deal with cuts, or something like a "rule of inference" or "logical axiom" that deals with them (even in special cases)? – jweightman Oct 07 '22 at 21:19
  • 1
    @jweightman: Just glossed over *A Declarative Semantics for the Prolog Cut Operator.* and the example given is `remove/3` which can be much better expressed with `if_/3` as it is then also usable in "all directions". I'd say it is a waste of time to look after these cut worshipers. – false Oct 07 '22 at 21:36
  • Thinking over your answer a bit more, I take issue with this claim: "But to have a declarative semantics, conjunction must be commutative." A programming language is declarative if programs do not explicitly define control flow, so one can construct a declarative language from any calculus or formal logic. I don't think it's that unreasonable to consider formal logics with the axioms that do not entail commutativity of conjunction, for the same reason that axiomatizations of intuitionistic logic do not entail the law of excluded middle in general. – jweightman Oct 13 '22 at 19:08
  • To be a bit more constructive, are there _any_ properties of “cut” that hold in general? Based on your answer and thinking a bit more about the problem, I think the answer is “no.” Alternatively, perhaps there are things that are similar to cut in certain respects that do. – jweightman Oct 13 '22 at 19:14
  • Look, you are questioning commutativity of conjunction. – false Oct 14 '22 at 17:17
  • Any discussion about a logical connective must take place in the context of a particular logic, and conjunction is a logical connective. I have never doubted the commutativity of conjunction in classical or intuitionistic logic. If you would like to improve your answer to fully answer the question, please address the last sentence: "are there extensions to these logics that make it possible to implement cut?" – jweightman Oct 15 '22 at 18:28
0

"Purely for performance"?

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

brebs
  • 3,462
  • 2
  • 3
  • 12
  • Fair enough, cuts have other uses. I've updated this statement in the question, but this isn't an answer to the question that I asked. – jweightman Oct 07 '22 at 15:45