Правильная работа программ

[Qlin]

Предположим, я использую в своей программе алгоритм, истинность которого доказана методом математической индукции. Почему этот алгоритм даёт правильный результат? С математической точки зрения алгоритм является верным, поскольку может быть доказан по индукции. Но почему должна правильно работать программа, которая его использует?

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

Доказать можно вообще всё, что угодно. Имеется бесконечное число всевозможных аксиоматик, в каждой из которых можно доказать что-то, что опровергается в другой. Но у программы есть ровно два варианта поведения: либо работа программы приводит к ожидаемому результату, либо — нет.

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

[alesha_popovich]

Так вы определитесь сначала, что для вас означает, что программа работает "правильно", иными словами, как вы интерпретирует результаты ее работы. Ибо при одной интерпретации результата одна и та же программа будет работать правильно, а при другой - нет. Вот тут то у вас и встанет все на свои места.

[Dmitriy40]

Qlin в сообщении #1374586 писал(а):

Предположим, я использую в своей программе алгоритм, истинность которого доказана методом математической индукции. Почему этот алгоритм даёт правильный результат? С математической точки зрения алгоритм является верным, поскольку может быть доказан по индукции. Но почему должна правильно работать программа, которая его использует?

Может быть потому что Вы пока не наткнулись на задачу, которая не реализуема машиной Тьюринга (см. Полнота по Тьюрингу)? Т.е. не вышли за рамки класса тьюринг-полных алгоритмов, которые все базируются на одной аксиоматике? Или потому что ваши алгоритмы уже автоматом привязаны к некоей аксиоматике, точно реализуемой машиной Тьюринга и соответственно программой на тьюринг-полном языке программирования? Собственно даже само понятие Алгоритм у Вас может быть ограничено лишь реализуемыми алгоритмами ...

Qlin в сообщении #1374586 писал(а):

Но у программы есть ровно два варианта поведения: либо работа программы приводит к ожидаемому результату, либо — нет.

Ну это не совсем верно, есть и третий вариант: бесконечное ожидание. Т.е. программа не выдаёт ни ожидаемый результат, ни его отрицание за конечное время. См.: Алгоритмическая разрешимость, Алгоритмически неразрешимая задача, Проблема остановки, Константа Хайтина.

[slavav]

Мне в решении этих вопросов помогла книга Дэвида Гриса "Наука программирования". Для каждого оператора языка программирования определяется его точная семантика в терминах предусловий и постусловий (речь об императивном языке). Получается аксиоматика, привязанная к конкретному языку. На основании аксиом доказываются теоремы для процедур. Также на языке пред- и постусловий. В конце концов вы доказываете теорему для всей программы: если входные данные отвечают таким-то предусловиям, то выходные отвечают таким-то постусловиям.
Полная цепочка: постановка задачи, перевод задачи на язык пред- и постусловий, написание программы, доказательство теоремы.

Есть более формальная и фундаментальная книга Эдсгера Дейкстры "Дисциплина программирования".
Обе книги довольно старые, но основы с тех пор не поменялись. После прочтения вы по-новому взгляните на языки программирования.

[alex55555]

Qlin в сообщении #1374586 писал(а):

Я перестал понимать, как связана математическая доказуемость с работоспособностью, и связана ли вообще.

Если доказательство исходит из тех же аксиом и теорем, что и процедурная модель исполнения программы, то можно доказывать, что программа будет работоспособной (или нет) в рамках данной аксиоматики.

Смысл задаётся ограничениями, а программа просто оперирует в рамках ограничений, а программист доказывает, что в рамках общих и для его теории и для программы ограничений результат будет именно ожидаемым.

[george66]

Почему не падают дома, построенные с учётом законов физики? Если придумать какие-нибудь другие законы физики и на них строить дома, будут ли они падать? Если не вникать глубоко, принцип математической индукции работает, потому что правильно отражает суть вещей.

[warlock66613]

Dmitriy40 в сообщении #1374596 писал(а):

Ну это не совсем верно, есть и третий вариант: бесконечное ожидание. Т.е. программа не выдаёт ни ожидаемый результат, ни его отрицание за конечное время.

Потенциально при некоторых предположениях есть ещё и четвёртый: программа выдаёт ожидаемый результат за нестандартное конечное время (подразумевается нестандартная модель арифметики первого порядка).

[realeugene]

warlock66613 в сообщении #1383286 писал(а):

Потенциально при некоторых предположениях есть ещё и четвёртый: программа выдаёт ожидаемый результат за нестандартное конечное время (подразумевается нестандартная модель арифметики первого порядка).

Выглядит как шутка.

-- 21.03.2019, 11:31 --

Qlin в сообщении #1374586 писал(а):

Но почему должна правильно работать программа, которая его использует?

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

[arseniiv]

realeugene в сообщении #1383291 писал(а):

Выглядит как шутка.

А для меня с некоторого времени это выглядит несколько апокалиптично, но точно не как шутка.

Кстати специально зашёл, перечитав в цитатнике это:

Qlin в сообщении #1374586 писал(а):

Если в арифметике заменить схему аксиом индукции на какую-либо другую схему аксиом, то получится другая теория

…которую нельзя будет звать теорией, говорящей про $\mathbb N$. Конкретный вид индукции для $\mathbb N$ становится совершенно необходимым, если понимать $\mathbb N$ как индуктивный тип с двумя конструкторами ($0$ и $S$). Параллельно это отражается и в аппарате рекурсивных функций (конструкторы — это единственные интересные функции среди основных примитивно рекурсивных, а оператор примитивной рекурсии связан с индукцией). В частности этот аппарат*, и аксиомы Пеано, можно переписать для любого другого достаточно простого индуктивного типа (в общем случае не пробовал, но если ограничиться типом $A$ с конструкторами типов $A^n\to A$, то точно).

* Совсем оффтоп: ещё машины Минского — они мне очень понравились, а в интернете кто-то (в другом месте) был неправ, что они определимы только для вычислений с $\mathbb N$ и якобы потому хуже для преподавания чем те же машины Тьюринга (что $\mathbb N$ будет поставлено впереди остальных пространств конструктивных объектов). Пф, глупости. Ну вот хоть участники этого форума будут знать.

-- Чт мар 21, 2019 14:33:32 --

Мне просто немного жалко, что такие важные вещи не говорят обычно там же, где говорят про PA или вычислимость. Ну ясно, что индуктивные типы вводить — это надо отвлекаться и надолго, но в общем можно говорить просто об алгебре термов, например, и всё это уже старо как мир, чтобы пугаться, не знаю. А то потом приходит человек и говорит «заменим аксиомы индукции».

[warlock66613]

realeugene в сообщении #1383291 писал(а):

Выглядит как шутка.

Ну, если вы настолько чётко понимаете взаимосвязь между математическими теориями, формальными теориями разных порядков, их моделями и физическими моделями реальности, что это для вас просто шутка, то я могу только порадоваться за вас. Но про себя я такого сказать не могу. Так что для меня это не просто шутка, но нечто, чего я не понимаю, а хотелось бы (хотя бы на уровне "что разные компетентные люди думают по этому поводу").

[realeugene]

arseniiv
warlock66613

Насколько мне известно, до сих пор экспериментально наблюдались только натуральные числа из стандартной модели арифметики.
Здравый смысл-то не нужно терять. Речь идёт про совершенно физическую величину - число тактов процессора, которые он потратит на выполнение программы до её остановки. Остановка-то произойдёт в любом случае, только, возможно, электричество отрубят до нормального завершения работы алгоритма.

-- 21.03.2019, 14:46 --

arseniiv в сообщении #1383306 писал(а):

ещё машины Минского

А чё, тезис Чёрча уже опровергнут?

[arseniiv]

Зачем его опровергать, у них там «нашли» методические недостатки.

realeugene в сообщении #1383333 писал(а):

Насколько мне известно, до сих пор экспериментально наблюдались только натуральные числа из стандартной модели арифметики.

Я думал, мы о теории.

[realeugene]

arseniiv в сообщении #1383381 писал(а):

Зачем его опровергать, у них там «нашли» методические недостатки.

У кого "у них"? Он же в принципе недоказуем.

arseniiv в сообщении #1383381 писал(а):

Я думал, мы о теории.

Да тема вроде бы о "программах". Потому и весело было прочитать про "нестандартную модель арифметики". Стругацких напомнило.

[arseniiv]

realeugene в сообщении #1383383 писал(а):

У кого "у них"? Он же в принципе недоказуем.

Тогда я не понял, про что вы спросили в тот раз.

realeugene в сообщении #1383383 писал(а):

Да тема вроде бы о "программах".

Ну чтобы доказать, что программа будет работать правильно, нужно будет всё рассматривать в какой-то модели вычислений, это математика чистой воды.

[realeugene]

arseniiv в сообщении #1383387 писал(а):

Тогда я не понял, про что вы спросили в тот раз.

С противопоставлением моделей вычислений.

arseniiv в сообщении #1383387 писал(а):

Ну чтобы доказать, что программа будет работать правильно, нужно будет всё рассматривать в какой-то модели вычислений, это математика чистой воды.

Математика, в которой совершенно излишне углубляться в нестандартные модели арифметики и ограничивать себя логикой первого порядка. В конце концов, рассматриваемые модели вычислений предназначены для моделирования программ на компьютерах, работающих в реальном мире со стандартной моделью арифметики. Если, конечно, речь не идёт про исследования самой логики.