Interesting, but this doesn't solve my problem.
I really want the infinite precision number pi, so I need a formula that I can push harder on any time I need more bits. A cache of existing bits can speed up the process initially, but eventually I'll have to rely on the formula.
Thus, once I have _one_ such formula for pi, I can use the system itself to test other formulas for pi for guaranteed convergence intervals.
Suppose I have rational numbers r1, r2 such that r1<pi<r2; i.e., pi in (r1,r2). Then if I have to compare this "number" with another "number" (r3,r4), I can get several results:
(r1,r2) < (r3,r4) => "definitely yes", "definitely no", "need more bits from (r1,r2)", "need more bits from (r3,r4)".
Needless to say, comparing an accurate formula for upper & lower bounds will loop forever, since there will never be enough bits.
But since we know pi is irrational, we can always compare it with a rational number & it will terminate.
At 04:44 PM 3/5/2013, Richard Fateman wrote:
>On 3/5/2013 4:24 PM, Henry Baker wrote:
>>I've got the Lisp code for ordered unions of disjoint intervals working pretty reliably.
>>
>>The inference capability is reasonable:
>>
>>Given (if zerop(x-3) then 9 else 10) = 9, the system can deduce that x=3.
>>
>>Also, (if plusp(x) then x*x else x*x) >=0 is always true (for real x).
>>
>>Similarly, (if plusp(x) then x else -x) >=0 is always true (for real x).
>>
>>I found that _half-intervals_, e.g., x<3 or x<=3 are interesting & useful in their own right, and not just as
>>the lower or upper bound of a full interval 0<x<=3.
>>
>>Things to be done: rational approximations to real intervals: e.g., how to represent intervals like [-pi..pi), when pi itself is approximated by an interval with rational endpoints, which approximation might want to be automagically improved when necessary -- e.g., when comparing "pi)" with a half-interval like "22/7)".
>
>Well here's a way of dealing with pi... maybe too hackish for your taste.
>I have a nicer way based on a formula from Bill Gosper..
>Anyway here's the
>I took it out of my perhaps forthcoming Maxima implementation of interval arithmetic.
>
>;;; some stuff dealing with pi
>;;;
>(setf *pi333* 54971606468298087752956649260810266548667957980587204204356455828289234687359429673775107185983813579)
>;; if you want n bits of pi as a rational number, try (apple-pi n). n< 333.
>
>(defun apple-pi(n) (if (< n 333) (/ (ash *pi333* (- n 333)) (expt 2 n))
> (error "Only 333 bits of pi are stored at the moment")))
>
>;;; this next program produces an interval around pi. Calls a
>;;; function [actually a constructor for the type ri, real interval]
>;;; with the lower and upper bounds.
>
>(defun apple-pint(n)(if (< n 333)
> (let ((v (ash *pi333* (- n 333)))
> (d (expt 2 n)))
> (ri (/ v d) (/ (1+ v) d)))
> (error "Only 333 bits of pi are stored at the moment")))
>
>;;; obviously more digits of pi can be computed on the fly etc etc, and
>;;; it would be nicer to not have 333 hard-coded in about 6 places.
>;;; but you get the idea. And for people who are dealing with IEEE floats
>;;; whose fraction-lengths are, in extended, 64, and maybe in some
>;;; quad format might go to 256, then this is sufficient.
>
>;;;RJF