Two recursive containment rules have identical logical readings, but one fails to terminate - how can clause and goal order decide that?

## Two readings of the same clause Every clause in a logic program has two readings, and this question lives in the gap between them. The **declarative reading** says what the clause means: the head holds whenever the body goals all hold. Conjunction is commutative, so reordering the body changes nothing about the set of true instances. Two clauses in either program order define exactly the same relation. The **procedural reading** says what the engine will do: solve the goals left to right, try clauses top to bottom, descend depth first, and backtrack on failure. That reading is highly order-sensitive. Kowalski's formulation is the standard name for this split - **algorithm = logic + control**. The programmer supplies the logic; the engine supplies a fixed control strategy; termination and cost are properties of the pair, not of either alone. It is why a logic program can be perfectly correct as a specification and useless as a program. ## Why the recursive-goal-first variant diverges Consider the transitive closure of containment written both ways, with the same non-recursive base clause in each. In the variant whose body begins with the recursive goal, solving `partOf(cabinet, X)` immediately raises `partOf(cabinet, Middle)` - the **same** first argument, and a second argument that is, if anything, less constrained than before. That subgoal raises the same subgoal again, forever. Nothing in the descent gets smaller, and the engine has no notion that it has seen this goal before. The important nuance, and the thing an interviewer will push on, is *when* the divergence shows up. If the base clause is tried first, the query happily prints the answers reachable through it and only loops when those are exhausted - that is, when you ask for one answer too many, or when you pose a query that has no answer. A program that 'works' in a demo and hangs the first time a part is genuinely absent is exactly this defect. In the variant whose body begins with the fact goal, the recursive call is made with an argument that a fact has already bound, so each level descends one real step into finite data and the search terminates. ## Cycles are a separate failure Ordering fixes the shape of the recursion; it does not fix the data. If the facts contain a cycle - a housing recorded as containing a bracket that is recorded as containing the housing - a correctly ordered rule still walks round it forever, because each step is a genuine step and there is always another one. The usual repair is to thread the set of components already visited on this branch through the recursion and refuse to re-enter one. That repair is worth naming honestly: it is **control leaking into the logic**. The visited set says nothing about what containment means; it exists solely to steer the engine's search. A reviewer who sees an accumulator like that in a rule should read it as a signal that the declarative reading and the operational one have come apart. ## What actually changes termination | lever | changes the meaning? | changes termination? | |---|---|---| | swapping two goals in a body | no | yes | | swapping two clauses of a relation | no | yes, and answer order too | | adding a visited-set argument | yes, slightly - the relation now takes it | yes, on cyclic data | | the engine's search strategy | no | yes, and it is not yours to choose | That last row matters. Engines differ: some memoise goals, answering a repeated goal from a table rather than re-deriving it, and such an engine terminates on programs that a plain depth-first one loops on - including left-recursive definitions and cyclic data. Some offer bounded or iteratively deepened search. So 'does this program terminate' is not answerable from the clauses alone; it is answerable from the clauses plus the engine. ## How to work the problem in practice 1. Read the clause declaratively first and confirm the relation is the one you meant. If the logic is wrong, no ordering saves it. 2. Then read it procedurally: for each recursive goal, name what is strictly more constrained than in the caller. If you cannot name anything, the descent is unbounded. 3. Reorder so that a goal which consults the facts runs before the recursive goal, so every recursive call is made on something bound. 4. Ask whether the data can cycle. If it can, add the visited set and accept that it is control, not logic. The broader lesson generalises past this paradigm: whenever a language lets you state intent and hands execution to an engine, correctness of the statement is not sufficiency. Something still chooses the order, and if you cannot say what that something does, you cannot predict whether your program finishes.