P1 = enum(P0) = {mary11(3), mary12(3), mary21(3), mary22(3)}.
P2 = enum(P1) = {}.
Since P2 is empty, the computation cycle will restart with P0 reset to the current value of P1. The new P1 will grow larger but all its elements will again be eliminated. Even though P1 keeps growing all subsequent P2 will be empty. Therefore the abstract machine M will never halt.
Question: If we change the enum() function as follows:
The enum() function maps a predecessor element x(t1) with age t1
to produce two successor elements x1(1) and x2(1) with age 1.
Will the abstract machine M ever halt?
What other problems may appear?
Answer: If the input P0 is {john(2), mary(1)}
the machine M will halt. However if the
input P0 is the empty set {}, the machine M will never halt.