= Solution
First find a sign bracket by <exponential search>, then bisect that bracket without evaluating its endpoints again:
``
def floorRoot(): Int = {
require(eval(0.0) < 0.0)
var lo = 0
var hi = 1
while (eval(hi.toDouble) <= 0.0) {
lo = hi
require(hi <= Int.MaxValue / 2, "doubling bound exceeds Int range")
hi *= 2
}
while (hi - lo > 1) {
val mid = lo + (hi - lo) / 2
if (eval(mid.toDouble) <= 0.0) lo = mid
else hi = mid
}
lo
}
``
For the first <while loop> the <loop invariant> is $p(\mathrm{lo})\leq0$, with `hi` a positive power of two, and either $(\mathrm{lo},\mathrm{hi})=(0,1)$ or $\mathrm{hi}=2\mathrm{lo}$. Every previously tested power of two has nonpositive value. Let $t$ be the least nonnegative <integer> for which $p(2^t)>0$. It exists by the positive <leading coefficient>. If the current upper endpoint is $2^k$, a mathematical <loop variant> is $t-k$ while the guard holds; the next doubling decreases it by one. The first <while loop>'s <postcondition> is $p(\mathrm{lo})\leq0<p(\mathrm{hi})$. The second <while loop> has exactly the invariant, variant and adjacent-integer <postcondition> established in part c.
There are $t+1$ evaluations at powers of two. If $t\geq1$, the final bracket has width $2^{t-1}$ and takes exactly $t-1$ midpoint evaluations. Including the initial sign check, the total is \b[$2t+1$ evaluations for $t\geq1$, and two for $t=0$]. Thus evaluation cost is $O(\log U)$ for the first positive dyadic bound $U=2^t$; it is not a claim about the first positive <root of a polynomial> when the <polynomial> is nonmonotone.
The mathematical argument uses unbounded <integer> endpoints and reliable signs. The guarded `Int` implementation requires the successful dyadic bound to fit in `Int`; otherwise it explicitly fails rather than wrapping to a negative bound. The coefficient assumptions alone cannot guarantee that a requested <integer> result fits a fixed-width type. Floating-point overflow or unreliable signs likewise need a wider or certified evaluator for a fully general implementation.
Back to article page
