Доказательство алгоритма вычисление многочлена

[Gts]

Есть многочлен $P(x) = a_nx^n + a_{n - 1}x^{n - 1} + \dots + a_1x + a_0$
Есть псевдокод, вычисляющий этот многочлен:

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

Нужно доказать правильность этого алгоритма.
Я делаю это так: инвариант цикла будет $(p_i = p_{i+1}x + Ai) and (n-1 \leqslant i \leqslant 0)$. Инвариант будет истинным перед каждой итерацией. Условие завершение цикла $i < 0$, что у нас в коде достигается. Так как инвариант и условие завершение цикла истинны, то наш код правильный.
Здесь есть ошибки?



Также я хочу доказать правильность этого кода с помощью математический индукции. Как можно найти формулу суммы всех членов многочлена?

[iifat]

Это не инвариант

[Gts]

iifat в сообщении #984246 писал(а):

Это не инвариант

Вы меня озадачили. А что же будет инвариантом для этого цикла?

[mihailm]

Gts, название функции на русский перевести сможете?

[arseniiv]

Gts в сообщении #984233 писал(а):

Также я хочу доказать правильность этого кода с помощью математический индукции. Как можно найти формулу суммы всех членов многочлена?

Так вот же она:

Gts в сообщении #984233 писал(а):

$P(x) = a_nx^n + a_{n - 1}x^{n - 1} + \dots + a_1x + a_0$

Индукция по $n:n\geqslant\deg P$ — это правильно! Правда, ваш псевдокод не сработает с $n=0$. Ну ладно, тут можно начинать и с единицы.

[Gts]

mihailm в сообщении #984302 писал(а):

Gts, название функции на русский перевести сможете?

Гуглом перевёл - "горнист". Я пока не понимаю куда Вы клоните.

Цитата:

Правда, ваш псевдокод не сработает с $n=0$. Ну ладно, тут можно начинать и с единицы.

Это код с "Алгоритмов" Скиены.

Цитата:

Индукция по $n:n\geqslant\deg P$ — это правильно!

n больше либо равно степенной P? Я просто не встречался с обозначением deg, но судя по гуглу это как-то со степенью связано. Пока я не понял, что Вы написали.

[arseniiv]

Степенью многочлена (это наибольшая из степеней переменной, при которой стоит ненулевой коэффициент). Многочлен задаётся $n$ коэффициентами $\Leftrightarrow$ его степень не больше $n$.

Gts в сообщении #984347 писал(а):

Гуглом перевёл - "горнист". Я пока не понимаю куда Вы клоните.

Наверно, клонил к схеме Горнера (это она и есть).

[iifat]

mihailm в сообщении #984302 писал(а):

название функции на русский перевести сможете?

Таки не вполне понимаю, о чём вы. «Схема Горнера» — не перевод названия функции. Да и даже б если и так, непонятно, о чём вы. Явно учебная задача на доказательство правильности программы. Наверняка, разумеется, она разобрана в каком-нить учебнике, но искать по названию — труд лет на пять, имхо.

Gts в сообщении #984267 писал(а):

А что же будет инвариантом для этого цикла?

В начале тела цикла у нас имеются: переменные $p$, $i$, массив $a$. Про них и должно быть высказывание-инвариант. Никаких $p_i$ в программе не имеется.

[Gts]

iifat в сообщении #984567 писал(а):

Gts в сообщении #984267 писал(а):

А что же будет инвариантом для этого цикла?

В начале тела цикла у нас имеются: переменные $p$, $i$, массив $a$. Про них и должно быть высказывание-инвариант. Никаких $p_i$ в программе не имеется.

У меня сильное сомнение, что так можно записать факт о том, что текущий элемент получается с помощью предыдущего, но больше я ничего не придумал. Как указать, что тут $=$ присваивание, а не равенство?
$(p = px + A_i) and (n-1 \geqslant i \geqslant 0)$


Теперь попробую с мат. индукцией доказать верность алгоритма.
База индукции. Положим $n=1$. Алгоритм нам даст $p = A_1 x + A_0$, что соответствует истине.

Делаем предположение, что алгоритм доказан для первых $k$ случаев.

Шаг индукции. Доказываем, что алгоритм верен для $k=n+1$ случаев.
Алгоритм у нас вычисляет $n$ элементов многочлена и для меня очевидно, что он сможет вычислить $n+1$ элементов. Как эту очевидность доказать до меня не доходит.

Есть вот такие мысли: мы сделали шаг индукции и получили многочлен $P_2$, заданный $n+1$ коэффициентами. И для него всё равно сохранилась истинность утверждения $n+1\geqslant\deg P_2$.

[iifat]

В математике нет присваиваний. Есть условия. В применении к доказательству программ условия записываются в местах перехода от оператора к оператору. Вот составьте блок-схему программы. Строго говоря, на каждой линии надо написать условие. Условия на линиях, входящих в блок оператора и выходящих из него , связаны соотношениями, зависящими от этого оператора.

[Gts]

Цитата:

условия записываются в местах перехода от оператора к оператору

Можете привести пример условий для вот этой программы?

def get_sum(a, b):
    x = a + b
    return x

Вот каждый оператор в отдельном блоке, но какие можно поставить условия на каждую линию оператора?..

[iifat]

Ну, во-первых, что такое $a+b$? Не припоминаю таких операторов.
Во-вторых, условие на первой стрелке $t$, то бишь никакого. На последней (у вас третья, но вторая лишняя) — $x=a+b$, только = тут, в отличие от Цэ, отношение равенства.

-- 04.03.2015, 02:13 --

Вот ещё пример:

Используется синтаксис C

int x = 0; for (int i = 1; i<10; i++) x+=i;

Условие после первого оператора, присваивания, $x=0$; условие в конце тела цикла $1\leq i \wedge i\le10 \wedge x=\sum_{k=1}^ik$

[Gts]

Цитата:

Ну, во-первых, что такое $a+b$? Не припоминаю таких операторов.

Оператор суммирования с операндами. :) Я Вас не так понял, про каждый оператор. Теперь начинаю понимать о каких условиях речь.

Цитата:

условие на первой стрелке $t$, то бишь никакого.

Суть понял, почему условие пустое. А $t$ это сокращение от какого-то слова?

Цитата:

Вот ещё пример:

Увидел пример и мелькнула мысль, что "вот оно!" У меня даже в мыслях не было, что тут можно использовать знак суммы. Я знал, что некоторые рекуррентные формулы представляются с помощью знака суммы, но не догадался, что это тут можно применить.
Но проблема как написать, что предыдущее p у нас используется в следующей итерации, пока осталась.
Итерации при $n=5$
$ A_5x + A_4 \\ (A_5x + A_4)x + A_3 \\ ((A_5x + A_4)x + A_3) x + A_2 \\ (((A_5x + A_4)x + A_3) x + A_2)x + A_1 \\ ((((A_5x + A_4)x + A_3) x + A_2)x + A_1)x + A_0 $



По поводу доказательства с помощью математической индукции возникла вот такая мысль.
Для удобства переделаем немного заголовок функции в псевдокоде так, чтобы мы могли передавать значение $n$.

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

База индукции. Положим $n=1$. Функция horner(A, x, 1) вернёт нам $p = A_1 x + A_0$, что есть истина.
Переход. Рассмотрим многочлен с $n+1$ коэффициентами и докажем для него, что $horner(A, x, n+1)$ вернёт $\sum\limits_{i=0}^{n+1}a_ix^i$
Докажем, что это так
$horner(A, x, n+1) = a_{n+1} x^{n+1} + horner(A, x, n) = a_{n+1} x^{n+1} + \sum\limits_{i=0}^{n}a_ix^i$ = \sum\limits_{i=0}^{n+1}a_ix^i
Моё доказательство с помощью мат. индукции верное?

-- 04.03.2015, 15:28 --

Цитата:

Моё доказательство с помощью мат. индукции верное?

Хотя, похоже это не совсем то что нужно. Тут скорее нужно доказать правильность цикла, а не относиться к функции, как к чёрному ящику и просто знать, что она считает.

[iifat]

Gts в сообщении #985513 писал(а):

$t$ это сокращение от какого-то слова?

true. Ну или 1. Пустое, в общем.

Gts в сообщении #985513 писал(а):

У меня даже в мыслях не было, что тут можно использовать знак суммы

Ну, я уже не помню конкретной теории. По духу, можно любые условия, ограничений никаких нет. Лишь бы каждое входящее влекло каждое выходящее с учётом оператора. Ну вот возьмите хоть мою программу, нарисуйте блок-схему (я б нарисовал, но с рисованием у меня не очень) и попробуйте на ней — только подробно, на каждой стрелке.

Gts в сообщении #985513 писал(а):

По поводу доказательства

Нет. Это не доказательство во-первых, и не то доказательство во-вторых. Вы пытаетесь доказать правильность схемы Горнера, а не программу.

[Gts]

Цитата:

Это не доказательство во-первых, и не то доказательство во-вторых. Вы пытаетесь доказать правильность схемы Горнера, а не программу.

Да, да. Это я понял.



Немного отступлю от темы:

Цитата:

Вы пытаетесь доказать правильность схемы Горнера

А допустим, что функция у нас считала сразу бы по формуле p=$\sum\limits_{i=0}^{n}a_ix^i$, то моё доказательство верное?