fool at sdf-eu.org fool at sdf-eu.org
Tue Sep 28 22:58:25 EDT 2004

```Hi.

> floorRootDef, floorRoot :: Integer -> Integer -> Integer
>
> floorRootDef k n | k>=1 && n>=1 = last (takeWhile (\x->x^k<=n) [1..])
>
> floorRoot k n | k>=1 && n>=1 = h n where
>   h x = let y=((k-1)*x+n`div`x^(k-1))`div`k in if y<x then h y else x

(Oddly enough, you get an iteration formula for the _floor_ of the
k-th root just by putting _floor_ brackets around every quotient in
Newton's iteration formula for the k-th root.)

Exercise: Transform floorRootDef into floorRoot by
extensional-equality-preserving steps.  I don't know how to do this.

To conventionally prove the correctness of floorRoot, it suffices to
show for all integers k>=1, n>=1, x>=1, y:=[((k-1)*x+[n/x^(k-1)])/k],
r:=[n^(1/k)] ([] denoting floor):
(1)  r<=y    (so r<=x is preserved in the iteration)
and
(2)  x<=y --> x<=r    (so r<=x<=r when the break condition is met).
Using
a<=[b] <--> a<=b
for all integers a and reals b, (2) is straightforward
and (1) is equivalent to
k*r-(k-1)*x <= n/x^(k-1),
which by r^k<=n can be sharpened to
(3)  k*(r-x)+x <= r^k/x^(k-1),
which is true by induction over k if (3) implies
k*(r-x)+x + r-x <= r^k/x^(k-1) * r/x,
which indeed by (3) can be sharpened to
k*(r-x)+r <= (k*(r-x)+x)*r/x,
equivalently (multiply by x and collect terms)
0 <= k*(r-x)^2, done.

--
fool at sdf-eu.org
SDF-EU Public Access UNIX System - http://sdf-eu.org
```