Naive reverse is the classic Prolog benchmark: it reverses a 30-element list with a deliberately inefficient program, so every implementation does the same amount of work. EyeProlog runs it, proves the result, and checks all 498 steps of that proof.
Run it in the playground · Source
What is the list [1, 2, ..., 30] backwards, and what does it cost to find
out with the textbook program?
The benchmark dates from Quintus Prolog in 1984. Systems were compared by how many of these logical inferences they performed per second (LIPS), so the program is chosen for predictable work, not for speed.
nrev([], []).
nrev([X|Rest], Ans) :-
nrev(Rest, L),
concatenate(L, [X], Ans).
concatenate([], L, L).
concatenate([X|L1], L2, [X|L3]) :-
concatenate(L1, L2, L3).
To reverse a list, reverse its tail and append the head at the end. Appending walks the whole reversed tail each time, so a list of length n costs about n²/2 concatenation steps.
data([1,2,3,4,5,6,7,8,9,10,
11,12,13,14,15,16,17,18,19,20,
21,22,23,24,25,26,27,28,29,30]).
bench_result(Reversed) :-
data(List),
nrev(List, Reversed).
The file also keeps the original harness predicates dobench/1 and
dodummy/1, which time many repetitions and subtract the cost of an empty
loop.
eyeprolog examples/bench.pl
bench_result([30, 29, 28, 27, 26, 25, 24, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1]).
eyeprolog --proof examples/bench.pl
step(nrev([30], [30]),
rule(2),
['X' = 30, 'Rest' = [], 'Ans' = [30], 'L' = []],
[nrev([], []), concatenate([], [30], [30])]).
step(nrev([], []), fact(1), [], []).
step(concatenate([], [30], [30]), fact(3), ['L' = [30]], []).
The innermost call reverses the one-element list [30]: reverse the empty
tail (fact 1), then append [30] to the empty list (fact 3). Every larger
reversal in the proof is built the same way, one level up.
condition('C1', resolution, ok, 498).
condition('C4', coverage, ok, 498).
condition('C7', relevance, ok, 499).
trusted(0).
verdict(checked).
The checker replays all 498 steps against the clauses they cite. No arithmetic or library call is involved, so nothing is taken on trust: the whole reversal is checked from the program alone.
data/1 to 40 elements. The checked proof grows from 498 to 863
steps: the quadratic cost is visible in the proof itself.nrev/2 with an accumulator version,
rev([X|Xs], A, R) :- rev(Xs, [X|A], R).. The same 30-element reversal
then needs only 34 checked steps.--goal 'nrev([a, b, c], R)' with --proof and count the steps. Can
you predict the count for a list of length n before running it?Learn more in The Art of EyeProlog, Chapters 5 and 23.