Writing a proof for an algorithm

Question

I am trying to compare 2 algorithms. I thought I may try and write a proof for them. (My math sucks, so hence the question.)

Normally in our math lesson last year we would be given a question like <can't use symbols in here so left them out>.

Prove: (2r + 3) = n (n + 4)

Then I would do the needed 4 stages and get the answer at the end.

Where I am stuck is proving prims and Kruskals - how can I get these algorithms in to a form like the mathmatical one above, so I can proceed to prove?

Note: I am not asking people to answer it for me - just help me get it in to a form where I can have a go myself.

Answer 1

You don't give many details but there is a community of mathematicians (Mathematical Knowledge Management MKM) who have developed tools to support computer proofs of mathematics. See, for example:

http://imps.mcmaster.ca/

and the latest conference

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

Answer 2

From my maths classes at Uni I (vaguely) remember proving Prims and Kruskals algorithms - and you don't attack it by writing it in a mathematical form. Instead, you take proven theories for Graphs and combine them e.g. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness to build the proof.

If your looking to prove the complexity, then simply by the working of the algorithm it's O(n^2). There are some optimisations for the special case where the graph is sparse which can reduce this to O(nlogn).

Answer 3

Where i am stuck is proving prims and Kruskals - how can i get these algorithms in to a form like the mathmatical one above so i can proceed to prove

I don't think you can directly. Instead, prove that both generate a MST, then prove that any two MST are equal ( or equivalent, since you can have more than one MST for some graphs ). If both algorithms generate MSTs which are shown to be equivalent, then the algorithms are equivalent.

Answer 4

To prove the correctness of an algorithm, you typically have to show (a) that it terminates and (b) that its output satisfies the specification of what you're trying to do. These two proofs will be rather different from the algebraic proofs you mention in your question. The key concept you need is mathematical induction. (It's recursion for proofs.)

Let's take quicksort as an example.

To prove that quicksort always terminates, you would first show that it terminates for input of length 1. (This is trivially true.) Then show that if it terminates for input of length up to n, then it will terminate for input of length n+1. Thanks to induction, this is sufficient to prove that the algorithm terminates for all input.

To prove that quicksort is correct, you must convert the specification of comparison sorting to precise mathematical language. We want the output to be a permutation of the input such that if i ≤ j then a_i ≤ a_j. Proving that the output of quicksort is a permutation of the input is easy, since it starts with the input and just swaps elements. Proving the second property is a little trickier, but again you can use induction.

Answer 5

Most of the times the proof depends on the problem you have in your hand. Simple argument can be suffice at times, at some other times you might need rigorous proof. I once used a corollary and proof of already proved theorem to justify my algorithm is right. But that is for a college project.

Answer 6

Maybe you want to try out a semi-automatic proof method. Just to go for something different ;) For example, if you have a Java specification of Prim's and Kruskal's algorithms, optimally building upon the same graph model, you can use the KeY Prover to prove the equivalence of the algorithm.

The crucial part is to formalize your proof obligation in Dynamic Logic (this is an extension of first-order logic with types and means of symbolic execution of Java programs). The formula to prove could match the following (sketchy) pattern:

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

This expresses that for all graphs, both algorithms terminate and the result is the same tree.

If you're lucky and your formula (and algorithm implementations) are right, then KeY can prove it automatically for you. If not, you might need to instantiate some quantified variables which makes it necessary to inspect the previous proof tree.

After having proven the thing with KeY, you can either be happy about having learned something or try to reconstruct a manual proof from the KeY proof - this can be a tedious task since KeY knows a lot of rules specific to Java which are not easy to comprehend. However, maybe you can do something like extracting an Herbrand disjunction from the terms that KeY used to instantiate existential quantifiers at the right-hand side of sequents in the proof.

Well, I think that KeY is an interesting tool and more people should get used to prove critical Java code using tools like that ;)