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
(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@sdf-eu.org SDF-EU Public Access UNIX System - http://sdf-eu.org