Написание доказательства для алгоритма

Question

Привет, ребята, я пытаюсь сравнить 2 алгоритма и подумал, что могу попытаться написать доказательство для них !!! (моя математика отстой, поэтому и возникает вопрос)

Обычно на нашем уроке математики в прошлом году нам задали вопрос типа

доказать: (2r + 3) = n (n + 4)

тогда я бы сделал необходимые 4 этапа и получил бы ответ в конце

Где я застрял, это проверяет простые числа и Крускала - как я могу привести эти алгоритмы в форму, подобную математической, приведенной выше, чтобы я мог приступить к доказательству

примечание: я не прошу, чтобы люди ответили за меня - просто помогите мне привести его в форму, в которой я сам смогу пойти

спасибо

Answer 1

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

Давайте возьмем быструю сортировку в качестве примера.

Чтобы доказать, что быстрая сортировка всегда завершается, вы сначала должны показать, что она завершается для ввода длины 1. (Это тривиально верно.) Затем покажите, что если она завершается для ввода длины до n , затем он будет завершен для ввода длины n + 1 . Благодаря индукции этого достаточно, чтобы доказать, что алгоритм завершается для всех входных данных.

Чтобы доказать правильность быстрой сортировки, необходимо преобразовать спецификацию сортировки сравнения в точный математический язык. Мы хотим, чтобы выходные данные представляли собой перестановку входных данных, так что если i & le; j , затем a _i & le; а _J . Доказать, что вывод быстрой сортировки является перестановкой ввода, легко, поскольку он начинается с ввода и просто меняет элементы. Доказать второе свойство немного сложнее, но опять же вы можете использовать индукцию.

Answer 2

Вы не даете много подробностей, но есть сообщество математиков (Управление математическими знаниями MKM), которые разработали инструменты для поддержки компьютерных доказательств математики. Смотрите, например:

http://imps.mcmaster.ca/

и последняя конференция

http://www.orcca.on.ca/conferences/cicm09/mkm09/

Answer 3

Где я застрял, это проверяет простые числа и Крускала - как я могу привести эти алгоритмы в форму, подобную математической, приведенной выше, чтобы я мог приступить к доказательству

Я не думаю, что вы можете напрямую. Вместо этого докажите, что оба генерируют MST, а затем докажите, что любые два MST равны (или эквивалентны, поскольку вы можете иметь более одного MST для некоторых графов). Если оба алгоритма генерируют MST, которые показаны эквивалентными, то алгоритмы эквивалентны.

Answer 4

Может быть, вы хотите попробовать полуавтоматический метод доказательства. Просто чтобы перейти к чему-то другому;) Например, если у вас есть Java-спецификация алгоритмов Прима и Крускала, оптимально основанная на той же графовой модели, вы можете использовать KeY Prover , чтобы доказать эквивалентность алгоритма .

Важнейшая часть - формализовать ваше обязательство по доказательству в динамической логике (это расширение логики первого порядка с типами и средствами символического исполнения Java-программ). Формула для доказательства может соответствовать следующей (схематичной) схеме:

\forall Graph g. \exists Tree t.
    (<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t)

Это выражает то, что для всех графиков оба алгоритма завершаются, и результатом является одно и то же дерево.

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

После того, как вы доказали это с помощью KeY, вы можете либо порадоваться, узнав что-то, либо попытаться восстановить ручное доказательство из доказательства KeY - это может быть утомительным занятием, поскольку KeY знает множество правил, специфичных для Java, которые не легко понять. Однако, возможно, вы можете сделать что-то вроде извлечения дизъюнкции Гербранда из терминов, которые KeY использовал для создания экзистенциальных квантификаторов в правой части последовательностей в доказательстве.

Ну, я думаю, что KeY - интересный инструмент, и больше людей должны привыкнуть доказывать критический код Java с помощью таких инструментов;)

Answer 5

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

Answer 6

Из моих уроков математики в Uni я (смутно) помню, как проверял алгоритмы Примса и Крускала - и вы не нападаете на него, записывая его в математической форме. Вместо этого вы берете проверенные теории для графов и объединяете их, например. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness, чтобы построить доказательство.

Если вы хотите доказать сложность, то просто с помощью алгоритма это O (n ^ 2). Существуют некоторые оптимизации для особого случая, когда график разрежен, что может уменьшить это значение до O (nlogn).