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

Question

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

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

доказать: (2г + 3) = п (п + 4)

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

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

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

благодаря

Answer 1

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

http://imps.mcmaster.ca/

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

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

Answer 2

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

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

Answer 3

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

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

Answer 4

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

В качестве примера возьмем quicksort.

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

Чтобы доказать, что быстрая сортировка верна, вы должны преобразовать спецификацию сортировки сортировки на точный математический язык. Мы хотим, чтобы выход быть permutation входа таким образом, что если я ≤ J затем в _я ≤ _J. Доказательство того, что выход quicksort является перестановкой ввода, прост, так как он начинается с ввода и просто свопирует элементы. Доказательство второго свойства немного сложнее, но снова вы можете использовать индукцию.

Answer 5

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

Answer 6

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

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

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

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

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

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

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