The deep-taxonomy benchmark at depth 10000: 30,000 chain rules, each step depending on the one before. At this depth the recursion itself is the test: the answer needs 10,000 nested subgoals. Siblings: 10, 100, 1000, 100000.
Run it in the playground · Source
ind is in n0, each of 10,000 levels lifts it one class higher, and
n10000 implies a2. Is ind in a2?
Proving a(ind, a2) asks for a(ind, n10000), which asks for
a(ind, n9999), and so on, ten thousand levels deep. An implementation that
used one native stack frame per level could overflow here.
a(ind, n0).
a(X, a2) :- a(X, n10000).
a(X, n1) :- a(X, n0).
a(X, i1) :- a(X, n0).
a(X, j1) :- a(X, n0).
eyeprolog examples/deep-taxonomy-10000.pl
a(ind, a2).
eyeprolog --stats reports a maximum depth of 10001. EyeProlog’s solver is
iterative, so a deep chain costs memory, not native stack.
step(a(ind, a2), rule(4), ['X' = ind], [a(ind, n10000)]).
step(a(ind, n10000), rule(30002), ['X' = ind], [a(ind, n9999)]).
10,002 steps and 10,002 cited clauses. The proof file is about 1.2 MB, yet every line is one small, independently checkable claim.
condition('C1', resolution, ok, 10002).
condition('C2', well_founded, ok, 10002).
condition('C4', coverage, ok, 10002).
steps(10002).
trusted(0).
verdict(checked).
C2 (well-foundedness) matters at this depth: the checker confirms that the 10,002 steps form a chain that ends in a fact and never loops back on itself.
--stats and compare max_depth with the depth-1000 version.--goal 'a(ind, n5000)'. How many steps does its proof need?--check-proof of its proof. Which is faster, and why
might checking be cheaper than finding?Learn more in The Art of EyeProlog, Chapters 13 and 16.