√2 has the continued fraction [1; 2, 2, 2, …]. Cutting it off after more and more terms gives better and better fractions, its convergents. A two-line recurrence generates them, and a table keeps the recurrence fast.
Run it in the playground · Source
What is the 10th, and the 15th, convergent P/Q of √2? How good is it?
For these convergents there is a neat measure of quality: P² − 2Q² is always +1 or −1. That is Pell’s equation, and it says that P/Q squared is as close to 2 as a fraction with denominator Q can get.
:- table conv/3.
conv(0, 1, 1).
conv(1, 3, 2).
conv(N, P, Q) :-
(N > 1),
(N1 is N - 1),
(N2 is N - 2),
conv(N1, P1, Q1),
conv(N2, P2, Q2),
(Twicep1 is 2 * P1),
(P is Twicep1 + P2),
(Twiceq1 is 2 * Q1),
(Q is Twiceq1 + Q2).
Each numerator is twice the previous one plus the one before that, and the
same holds for denominators. Like Fibonacci, the plain recurrence asks for the
same earlier convergents again and again. :- table conv/3. makes EyeProlog
remember each answer, so every convergent is computed once.
pell_error(N, Error) :-
conv(N, P, Q),
(P2 is P * P),
(Q2 is Q * Q),
(Twiceq2 is 2 * Q2),
(Error is P2 - Twiceq2).
pell_error/2 turns the claim “P² − 2Q² = ±1” into something you can compute
for any convergent.
eyeprolog examples/continued-fraction-sqrt2.pl
convergent_answer(convergent_10, fraction(8119, 5741)).
convergent_answer(convergent_15, fraction(665857, 470832)).
convergent_answer(pell_error_15, 1).
convergent_answer(numerator_sum_0_to_10, 13859).
665857/470832 agrees with √2 to about eleven decimal places, and its Pell error is exactly 1. The last line adds up the numerators of convergents 0 to 10.
eyeprolog --proof examples/continued-fraction-sqrt2.pl
step(convergent_answer(pell_error_15, 1), rule(8), ['Error' = 1], [pell_error(15, 1)]).
step(sumall(Expression, (between(0, 10, N), conv(N, Expression, _q)), 13859), builtin, [], []).
The Pell error of 1 rests on pell_error(15, 1), which in turn rests on the
15th convergent and four arithmetic steps. The sum is different: it is
recorded as a single builtin step over a whole nested search.
eyeprolog --proof examples/continued-fraction-sqrt2.pl > cf.why.pl
eyeprolog --check-proof cf.why.pl examples/continued-fraction-sqrt2.pl
condition('C1', resolution, ok, 21).
condition('C5', re_decision, ok, 102).
obligation(builtin, theory_scoped, sumall(A, (between(0, 10, B), conv(B, A, C)), 13859)).
trusted(1).
verdict(checked_with_obligations).
The checker replays 21 clause steps and recomputes 102 arithmetic steps. The
sumall/3 step cannot be recomputed on its own, because its inner goal calls
conv/3, a predicate of this program. So it stays an obligation: the
answer holds provided that sum was collected correctly.
--goal 'pell_error(14, E)'. The error is −1: the sign alternates from
one convergent to the next.--goal 'conv(20, P, Q)' and compare P/Q with √2 on a calculator.:- table conv/3. and ask for conv(22, P, Q). The answer is the
same, but it takes seconds instead of a fraction of a second. Why does the
time grow so fast with N?Learn more in The Art of EyeProlog, Chapters 13 and 27.