Changeset 1238

Timestamp:

2015-06-11T14:56:03-07:00 (9 years ago)

Author:

Marek Rychlik

Message:

* empty log message *

File:

• branches/f4grobner/division.lisp (modified) (3 diffs)

branches/f4grobner/division.lisp

@@ -68 +68 @@
                                (ring (ro-ring ring-and-order))
                                (p-zero (make-poly-zero)))
-  "Loop invariant: c*f0=sum ai*fi+r+f, where f0 is the initial value of f"
+  "Check loop invariant of division algorithms, when we divide a
+polynomial F by the list of polynomials FL. The invariant is the
+identity C*F0=SUM AI*FI+R+F, where F0 is the initial value of F, A is
+the list of partial quotients, R is the intermediate value of the
+remainder, and F is the intermediate value which eventually becomes
+0."
   (flet ((p-add (p q) (poly-add ring-and-order p q))
          (p-sub (p q) (poly-sub ring-and-order p q))
@@ -80 +85 @@
                     f))))))
   
-
 
 (defun poly-pseudo-divide (ring-and-order f fl
@@ -94 +98 @@
 the quotients is initialized to default."
   (declare (type poly f) (list fl))
-  ;; Loop invariant: c*f0=sum ai*fi+r+f, where f0 is the initial value of f
+  ;; Loop invariant: c*f0=sum ai*fi+r+p, where f0 is the initial value of f
   (do ((r (make-poly-zero))
        (c (funcall (ring-unit ring)))