Code follows Scala 2 style. Each question uses its own enclosing declarations and the supplied fields; alternative implementations with the same name are separate solutions. Mathematical correctness arguments use exact values unless floating-point arithmetic or machine-range bounds are discussed explicitly.
Use Horner's method, accumulating the high-degree coefficients before the low-degree ones:
def eval(x: Double): Double = {
var i = a.length
var value = 0.0
while (i > 0) {
i -= 1
value = a(i) + x * value
}
value
}At each while loop head the loop invariant isThe initial sum is empty. Decreasing
i and replacing the accumulator by a(i) + x * value extends that sum by one coefficient with the required powers shifted. The loop variant is i; on exit it is zero, so the accumulator equals . The code uses exactly multiplications and time, with constant auxiliary space, and also handles the empty coefficient array as the zero polynomial. Initializing from the last coefficient instead would save one multiplication for nonempty arrays.The invariant is an exact-arithmetic specification. With
Double, each arithmetic operation rounds; consequently the code evaluates the Horner expression in floating-point arithmetic, rather than guaranteeing the exact real value for arbitrary coefficients.The coefficient assumptions imply a nonconstant polynomial with and a positive leading coefficient. Thus as : dividing by its leading power of leaves the positive leading coefficient plus terms tending to zero. There is some with . A polynomial is continuous, so the intermediate value theorem supplies at least one positive root of a polynomial in .
This gives neither uniqueness nor monotonicity. Multiple crossings are possible. If the degree of a polynomial is an even integer, the same leading-term argument gives as , so there is also a negative root of a polynomial. For an odd integer degree of a polynomial no negative root of a polynomial is forced; a linear polynomial with negative constant coefficient and positive slope is a counterexample.
Maintain opposite signs at the endpoints, rather than assuming that the polynomial is monotone:
def floorRoot(X: Int): Int = {
require(X > 0 && eval(0.0) <= 0.0 && eval(X.toDouble) > 0.0)
var lo = 0
var hi = X
while (hi - lo > 1) {
val mid = lo + (hi - lo) / 2
if (eval(mid.toDouble) <= 0.0) lo = mid
else hi = mid
}
lo
}The loop invariant is and . Both branches preserve those signs, even when there are other roots of a polynomial or sign reversals elsewhere. When the interval width exceeds one, the midpoint is strictly between its endpoints, so the positive integer loop variant
hi - lo strictly decreases. On exit hi == lo + 1, giving the required postcondition . Continuity establishes a root of a polynomial between those adjacent integers, possibly at the left endpoint.The width is at most halved with rounding upwards, so there are at most midpoint evaluations, plus two endpoint evaluations in the precondition check. The midpoint expression avoids adding two large endpoints. The explicit positive upper-bound precondition supplies the interval order assumed in the question. For the literal computed-
eval contract, the same proof holds provided evaluated midpoints are not NaN; identifying its bracket with the real polynomial additionally requires trustworthy evaluation signs.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 , with
hi a positive power of two, and either or . Every previously tested power of two has nonpositive value. Let be the least nonnegative integer for which . It exists by the positive leading coefficient. If the current upper endpoint is , a mathematical loop variant is while the guard holds; the next doubling decreases it by one. The first while loop's postcondition is . The second while loop has exactly the invariant, variant and adjacent-integer postcondition established in part c.There are evaluations at powers of two. If , the final bracket has width and takes exactly midpoint evaluations. Including the initial sign check, the total is evaluations for , and two for . Thus evaluation cost is for the first positive dyadic bound ; 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. Articles by others on the same topic
There are currently no matching articles.