eyeprolog

Computing π

How close does the Nilakantha series get to π?

The fifteenth-century Indian mathematician Nilakantha found a series for π that converges much faster than the better-known Leibniz series. This example sums it with a ten-thousand-level recursion, and the proof records every term.

Run it in the playground · Source

---

The question

The Nilakantha series is

π = 3 + 4/(2·3·4) − 4/(4·5·6) + 4/(6·7·8) − …

Summed term by term, how close does it get to π, and can every one of those thousands of steps be checked?

---

The program

pi(A, B) :-
    pi(1, A, 0, C, 1),
    B is 3+4*C.

pi(A, A, B, B, _) :-
    !.
pi(A, B, C, D, E) :-
    F is A+1,
    L is C+E/(2*A*(2*A+1)*(2*A+2)),
    M is -E,
    pi(F, B, L, D, M).

pi/5 carries a counter, the limit, the running sum, the result, and the sign. Each recursive call adds one term and flips the sign. When the counter reaches the limit, the first clause returns the sum, and pi/2 multiplies it by 4 and adds 3.

---

The answer

eyeprolog examples/pi.pl

pi(10000, 3.141592653590042).

The true value of π begins 3.141592653589793, so the result is correct to about twelve decimal places.

---

The reason

eyeprolog --proof examples/pi.pl

step(pi(10000, 3.141592653590042),
     rule(1),
     ['A' = 10000, 'B' = 3.141592653590042, 'C' = 0.03539816339751046],
     [pi(1, 10000, 0, 0.03539816339751046, 1), 3.141592653590042 is 3 + 4 * 0.03539816339751046]).

The answer is 3 + 4 × 0.0353981…, where that sum comes from the recursion. The next step down adds the first term, 1/(2·3·4) = 0.041666…, and the proof continues like this through all ten thousand levels.

---

The check

condition('C1', resolution, ok, 10001).
condition('C5', re_decision, ok, 20002).
steps(30003).
trusted(0).
verdict(checked).

The proof has 30,003 steps: 10,001 uses of the program’s clauses and 20,002 arithmetic steps, every one recomputed by the checker. A derivation ten thousand levels deep is replayed in full, with nothing taken on trust.

---

Try it

• Ask for pi(10, X) and pi(100, X). (EyeProlog gives 3.141839618929402 and 3.1415929035585526.) How many correct digits does each step of ten add?
• Write the Leibniz series π/4 = 1 − 1/3 + 1/5 − … in the same style, and compare the two at the same number of terms.
• The first clause uses a cut. Is it needed for the answer, or only to stop the search from looking further?

Learn more in The Art of EyeProlog, Chapters 6 and 26.

This site is open source. Improve this page.