2. Выявление общих принципов при дедукции Как убедиться, что принципы алгоритма верны? Либо мы проверяем принципы за счет большего количества вводных данных, либо, что более эффективно, находим точное математическое доказательство.
В философии есть утверждение, которое гласит, что правильность алгоритма не зависит от его выполнения. Другими словами, тестирование не может гарантировать правильность алгоритмов. Докажем это.
Вот основная линия доказательства:
1. Для всех учтенных вершин мы найдем кратчайшие пути.
2. Пункт назначения учитывается.
3. Следовательно, мы находим кратчайший путь к месту назначения.
Разве это не кажется вам знакомым? Например:
1. Все люди смертны.
2. Сократ – человек.
3. Следовательно, Сократ смертен.
На самом деле это силлогизм, классическая форма дедуктивного рассуждения. В основном это то, чем занимаются логики.
Еще один интересный исторический факт: формально концепция вычисления была впервые разработана логиками в 30-х годах ХХ века. Им нужно было знать, могут ли окончательно быть решены определенные логические задачи (чтобы избежать траты времени на решение чего-то неразрешимого). Для ответа на этот вопрос, они предложили идею вычислимости.
Позже в 1936 году Алонсо Чарч и Алан Тьюринг придумали формальное определение вычислимости (независимо друг от друга и в одно и то же время). В этой
статье дается исторический обзор вычислений.
Корректность вывода зависит от первых двух предпосылок. В нашем доказательстве вторая предпосылка очевидна, так как в алгоритме буквально учитываются все узлы. Однако, нам нужно доказать первую предпосылку, где мы находим кратчайший путь к узлу.
В этом может помочь математическая индукция. Это один из самых полезных методов для доказательства верности многих других алгоритмов.
Общая схема следующая. Первое — если алгоритм работает при значении равном 0. Второе — если алгоритм работает при значении равном n, подразумевается, что алгоритм действителен и со значением равным n + 1. Это значит, при входных данных, больших или равных 0, алгоритм работает. На этом этапе можно гарантировать верность алгоритма.
Чтобы убедиться в том, что алгоритм действительно рабочий, вы можете ознакомиться с данной
лекцией.
Замечу, что мы не должны путать математическую и философскую индукции. Математическая индукция является процессом дедуктивного мышления, поскольку ее верность содержится сама в себе, без каких-либо внешних наблюдений.
Когда мы придумываем алгоритм, он должен быть способным обрабатывать все возможные варианты выполнения примеров.
На практике тщательное математическое доказательство может быть не самой эффективной стратегией. Но по крайней мере мы можем рассмотреть как можно больше случаев выполнения, особенно противоречащих друг другу. Эта практика улучшит надежность нашего кода.
Возможно, вы заметили, что в нашем примере алгоритм поиска пути не работает, если вес ребра отрицательный. Причину этого можно найти в этой
лекции. Для обработки графика с отрицательным весом вы можете использовать
алгоритм Bellman-Ford.