[Maxima-discuss] removing assumptions such as prin-inf > 1.0e8 and lim-epsilon < 1.0e-8

[Barton W. <wi...@un...>]

The limit code and the definite integral code both make assumptions such as prin-inf > 1.0e8 and lim-epsilon < 1.0e-8.  Making and retracting these assumptions spawns a great deal of arithmetic. As an experiment, enter (trace(?simplus), limit(x)). Of the 99 calls to simplus, most of them are related to these assumptions.


Removing these assumptions to the limit code and the definite integral code allows the testsuite to run about 5% faster (in 190 seconds instead of about 200) and gives only three errors: we get nounforms for limit(floor(x),x,5,minus),  limit(floor(x),x,5,plus), and limit(floor(x),x,0).


Another experiment is


Standard Maxima:


(%i2) makelist(integrate(log(1+k/x^2),x,1,inf),k,1,100)$
Evaluation took 6.1000 seconds (6.1300 elapsed) using 545.458 MB.

(%i3) load("limit-assume.lisp")$

(%i4) makelist(integrate(log(1+k/x^2),x,1,inf),k,1,100)$
Evaluation took 3.6040 seconds (3.6000 elapsed) using 343.733 MB.

Eliminating the assumptions reduces the time from 6.1 seconds to 3.6 seconds.

--Barton

My file limit-assume.lisp is

(declare-top (special  limit-assumptions integer-info old-integer-info   *global-defint-assumptions*))

(defun make-limit-assumptions (var val direction)
  (let ((new-assumptions)); (use-old-context old-assumptions var val)))
;    (mapc #'assume new-assumptions)
    (cond ((or (null var) (null val))
       ())
      ((and (not (infinityp val)) (null direction))
       ())
      ((eq val '$inf)
       `(,(assume `((mgreaterp) ,var 0)) ,@new-assumptions))
      ((eq val '$minf)
       `(,(assume `((mgreaterp) 0 ,var)) ,@new-assumptions))
      ((eq direction '$plus)
       `(,(assume `((mgreaterp) ,var 0)) ,@new-assumptions)) ;All limits around 0
      ((eq direction '$minus)
       `(,(assume `((mgreaterp) 0 ,var)) ,@new-assumptions))
      (t
       ()))))

(defun restore-assumptions ()
;;;Hackery until assume and forget take reliable args. Nov. 9 1979.
;;;JIM.
  (do ((assumption-list limit-assumptions (cdr assumption-list)))
      ((null assumption-list) t)
    (forget (car assumption-list)))
  (forget '((mgreaterp) lim-epsilon 0))
  (forget '((mlessp) lim-epsilon 0))
  (forget '((mgreaterp) prin-inf 0))
  (cond ((and (not (null integer-info))
          (not limitp))
     (do ((list integer-info (cdr list)))
         ((null list) t)
       (i-$remove `(,(cadar list) ,(caddar list))))
     (setq integer-info old-integer-info))))

(defun make-global-assumptions ()
  (setq *global-defint-assumptions*
    (cons (assume '((mgreaterp) *z* 0))
          *global-defint-assumptions*))
  ;; *Z* is a "zero parameter" for this package.
  ;; Its also used to transform.
  ;;  limit(exp,var,val,dir) -- limit(exp,tvar,0,dir)
  (setq *global-defint-assumptions*
    (cons (assume '((mgreaterp) epsilon 0))
          *global-defint-assumptions*))
 ; (setq *global-defint-assumptions*
;    (cons (assume '((mlessp) epsilon 1.0e-8))
;          *global-defint-assumptions*))
  ;; EPSILON is used in principal value code to denote the familiar
  ;; mathematical entity.
  (setq *global-defint-assumptions*
    (cons (assume '((mgreaterp) prin-inf 0))
          *global-defint-assumptions*)))