On Wed, 23 Jul 2025 23:19:49 GMT, Raffaello Giulietti <rgiulie...@openjdk.org>
wrote:
>> @rgiulietti
>>> The Brent & Zimmermann paper assumes an initial estimate u ≥ ⌊ x 1 / n ⌋ ,
>>> probably for a (unstated) reason.
>>
>> The reason is the condition to stop the loop, since it terminates when the
>> estimate does not decrease anymore.
>>
>>>
>>> Given all of the above, we must ensure that the initial estimate meets the
>>> requirements of the BZ paper, or we need a proof that an underestimate in
>>> the 1st iteration is harmless because it will become an overestimate in the
>>> 2nd, i.e., that the reasoning which holds for the real-valued f also holds
>>> with the integer-valued analogous formula.
>>
>> In Brent & Zimmermann proof, we have the following definition: $f(t) := [
>> (n-1) t + m/t^{n-1}] / n$, with $t \in (0; +\infty)$. Since $f(t)' < 0$ if
>> $t < \sqrt[n]{m}$ and $f(t)' > 0$ if $t > \sqrt[n]{m}$, then $\sqrt[n]{m}$
>> is a point of minimum, so $f(t) \ge f(\sqrt[n]{m}) = \sqrt[n]{m}$, hence
>> $\lfloor f(t) \rfloor \ge \lfloor \sqrt[n]{m} \rfloor$ for any $t$ in the
>> domain. This proves that, when $\lfloor f(t) \rfloor \le \lfloor \sqrt[n]{m}
>> \rfloor$ becomes true (it does because the sequence of estimates is strictly
>> decreasing), we get $\lfloor f(t) \rfloor = \lfloor \sqrt[n]{m} \rfloor$ and
>> the loop stops at the next iteration.
>>
>>> The proof of the algorithm makes use of Newton's formula x i + 1 = f ( x i
>>> ) , where f is the real-valued counterpart of the integer recurrence
>>> formula in the algorithm. It is straightforward to see that x i + 1 > x 1 /
>>> n when 0 < x i < x 1 / n . But it's less clear to me that the same applies
>>> to the _integer_ recurrence formula of the algorithm.
>>
>> It should be clear if we note that the integer-valued analogous formula
>> simply discard the fraction part of the real-valued counterpart:
>> $\lfloor f(t) \rfloor = \lfloor [(n-1) t + m/t^{n-1}] / n \rfloor = \lfloor
>> \lfloor (n-1) t + m/t^{n-1} \rfloor / n \rfloor$
>>
>> So, if $x_i < \lfloor \sqrt[n]{m} \rfloor$, then $[(n-1) x_i + m/x_i^{n-1}]
>> / n > \sqrt[n]{m}$, hence $\lfloor f(x_i) \rfloor \ge \lfloor \sqrt[n]{m}
>> \rfloor$.
>>
>> From what has just been shown, it follows that it is sufficient to perform
>> an initial iteration before starting the loop to get an overestimate.
>
> Everything above is already present in BZ, except for your insight that
> $\lfloor f(s)\rfloor = \hat{f}(s)$, where $\hat{f}$ is the integer-valued
> recurrence function computed by the algorithm.
> So yes, this is a proof that an initial positive integer underestimate leads
> to a (weak) integer overestimate after one iteration. From then on, BZ shows
> termination and correctness.
>
> I think that a note in a comment like the following would be helpful:
> "The integer-valued recurrence formula in the algorithm of Brent&Zimmermann
> simply discard the fraction part of the real-valued Newton recurrence on f
> discussed in the referenced work. As a consequence, an initial underestimate
> (not discussed in BZ) will immediately lead to a (weak) overestimate during
> the 1st iteration, thus meeting BZ requirements for termination and
> correctness."
Correction:
"The integer-valued recurrence formula in the algorithm of Brent&Zimmermann
simply discards the fraction part of the real-valued Newton recurrence on f
discussed in the referenced work.
(Indeed, for real $x$ and integer $n > 0$, the equality $\lfloor x / n \rfloor
= \lfloor \lfloor x \rfloor / n \rfloor$ holds, from which the claim follows.)
As a consequence, an initial underestimate (not discussed in BZ) will
immediately lead to a (weak) overestimate during the 1st iteration, thus
meeting BZ requirements for termination and correctness."
-------------
PR Review Comment: https://git.openjdk.org/jdk/pull/24898#discussion_r2227858171
