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)".
>
> _______________________________________________
> Maxima mailing list
> Maxima at math.utexas.edu
> http://www.math.utexas.edu/mailman/listinfo/maxima
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