The Takeuchi function tak is a classic benchmark: three lines of recursion
that make an enormous number of calls. This example computes it with tabling,
so repeated calls are answered from a table, and keeps the arguments small
enough that the proof of the answer can be written out and checked.
Run it in the playground · Source
What is tak(16, 11, 6)?
Ikuo Takeuchi designed the function in 1978 to stress function calls. It
returns Z when X ≤ Y, and otherwise calls itself on three decremented,
rotated argument triples and then once more on their three results. Plain
recursion repeats the same subcalls again and again.
:- table tak/2.
tak([X, Y, Z], Z) :-
X =< Y,
!.
tak([X, Y, Z], A) :-
X1 is X-1,
tak([X1, Y, Z], A1),
Y1 is Y-1,
tak([Y1, Z, X], A2),
Z1 is Z-1,
tak([Z1, X, Y], A3),
tak([A1, A2, A3], A).
The three arguments travel as one list, so a call is tak([X, Y, Z], Result).
The :- table tak/2. declaration makes EyeProlog remember the answer of every
call pattern it has solved, so each distinct triple is computed once.
eyeprolog examples/takeuchi.pl
tak([16, 11, 6], 11).
According to the comment in the source, the tabled version answers in about
45 ms and the untabled one in about 250 ms. The gap grows quickly with the
arguments: tak([34, 13, 8], _) takes about 28 seconds without tabling.
step(tak([11, 11, 6], 6), rule(2), ['X' = 11, 'Y' = 11, 'Z' = 6], [11 =< 11, !]).
step(11 =< 11, builtin, [], []).
Each base case is one step: since 11 ≤ 11, tak returns its third argument,
6. The top-level answer rests on a tree of 249 such steps, each citing
clause 2 (the base case) or clause 3 (the recursion). Every distinct call
appears once, however often the search reached it.
condition('C1', resolution, ok, 198).
condition('C5', re_decision, ok, 51).
condition('C7', relevance, ok, 250).
steps(249).
verdict(checked).
The checker replays 198 rule steps and recomputes 51 built-in steps (the
subtractions, comparisons, and cuts) independently. The answer 11 is
checked, with nothing taken on trust.
:- table tak/2. line and time both versions.tak([18, 12, 6], A) and compare the size of its proof with the one
for [16, 11, 6].tak/2 for every triple with arguments between 0 and 6 using
findall/3. When does the result equal Y, and when Z?Learn more in The Art of EyeProlog, Chapter 13.