Cut operator scope when subsequent goals fail after unification succeeds
0 reputation · 19 Nov 2022, 11:29 UTC
Precise pruning boundary of the cut operator
In ISO Prolog and major implementations such as SWI-Prolog, the cut operator (!) discards choice points created since the parent goal was invoked. Unification of the clause head occurs before the cut is reached; if unification fails the cut is never executed and alternative clauses remain available. When unification succeeds but a later goal in the same clause fails, the cut has already removed the choice points for that clause and for any goals to its left.
The documentation states that the cut is local to the predicate in which it appears, yet the exact moment at which choice points are destroyed—relative to the failure of a goal positioned after the cut—affects whether the engine can backtrack into earlier disjunctions or sibling clauses. This boundary determines whether a program exhibits green-cut (efficiency-only) or red-cut (semantic-change) behavior.
Specific questions
- At what exact point in the execution sequence are choice points pruned when a cut is followed by a goal that subsequently fails?
- Does the pruning extend to choice points created by the parent goal before the current clause was entered, or only to those created within the current clause?
- Can a portable test distinguish green-cut from red-cut behavior without relying on implementation-specific tracing?