Есть многочлен P(x) = a _n * x ⁿ + a _{n — 1} * x ^{n — 1} + ... + a ₁ * x + a ₀
Есть псевдокод, вычисляющий этот многочлен:

function horner(A, x)
    p = A n
    for i from n - 1 to 0
        p = p * x + A i
    return p

Нужно доказать правильность этого алгоритма.
Я делаю это так: инвариант цикла будет (P = P * x + A _i) and (n — 1 >= i >= 0). Инвариант будет истинным перед каждой итерацией. Условие завершение цикла i < 0, что у нас в коде достигается. Так как инвариант и условие завершение цикла истинны, то наш код правильный.
Здесь есть ошибки?

Здравствуйте, Stgl, Вы писали:

S>Я делаю это так: инвариант цикла будет (P = P * x + A _i) and (n — 1 >= i >= 0). Инвариант будет истинным перед каждой итерацией. Условие завершение цикла i < 0, что у нас в коде достигается. Так как инвариант и условие завершение цикла истинны, то наш код правильный.
S>Здесь есть ошибки?

Инвариант записан как-то странно: P = P*x+A_i. Это что, уравнение такое? По переменной x? Поиск неподвижной точки?

Говоря о схеме Горнера, есть смысл перейти к последовательности многочленов
P(x) = SUM_i=0..n a_i*xⁱ
P(x) = P₀(x)
P_i(x) = P_i+1(x)*x + a_i
P_n+1(x) = 0
ну, или начать с
P_n(x) = 0*x + a_n

или, соответственно, к последовательности значений b_i этих многочленов для данного аргумента x
P(x) = b₀
P_i(x) = b_i = b_i+1*x+a_i
b_n+1 = 0
b_n = 0*x + a_n = a_n

Тогда надо будет лишь показать, что на i-й итерации цикла (где итерации нумеруются от n до 0 по убыванию) на входе b_i+1, на выходе b_i
В данном случае всё тривиально. Просто по определению.