# Proof of algorithm refinement

I recently had an interview in which I was asked to produce an algorithm to that computes the pairs of integers, from a list, that add up to a integer k. I then had to increase the time efficiency of this algorithm.

I have not studied algorithm before and from what I gather so far the efficient of an algorithm is mainly dependent on the initial structure of the data.

I figure its best to try an formalize the requirement using maths notation and then to redefine terms in ways that are more efficient to compute?

Here's my attempt to do this for the problem stated above.

a:= the algorithm

∃a∈((List,k)→Tsumk)(List⊆ℕ∧k∈ℕ∧Tsumk :={∀t∈(t1,t2)(k=t1+t2 ∧ t1,t2 ∈ List) | t})

refining Tsumk...

Tsumk := {∀i∈{0...k}(i,k ∈ ℕ ∧ k-i,k ∈ List) | (k-i,k)}

Now I need to prove that refined Tsumk is equivalent to original. By comparison... t=(k-i,k) therefore we need to prove ∀t∈(t1,t2)(k=t1+t2 ∧ t1,t2 ∈ List) ⇔ ∀i∈{0...k}(i,k ∈ ℕ ∧ k-i,k ∈ List)

To do this we can prove that the negation of the right hand side is⇔the negation of the right left hand side.

¬RHS = ¬(∀t∈(t1,t2)(k=t1+t2 ∧ t1,t2 ∈ List)) = ∃t∈(t1,t2)( ¬(k=t1+t2 ∧ t1,t2 ∈ List)))

¬LHS = ¬(∀i∈{0...k}(i,k ∈ ℕ ∧ k-i,k ∈ List)) = ∃i∈{0...k}( ¬(i,k ∈ ℕ ∧ k-i,k ∈ List))

let List = {0} let k = 0

¬(0=t1+t2 ∧ t1,t2 ∈ {0}))) ⇔ ¬(0,0 ∈ ℕ ∧ 0-0,0 ∈ List)

¬(0=t1+t2 ∧ t1,t2 ∈ {0}))) ⇔ ¬(T ∧ T)

let t1,t2=0 ¬(0=0+0 ∧ 0,0 ∈ List))) ⇔ ¬(T ∧ T)

¬(T ∧ T) ⇔ ¬(T ∧ T) = T

hence prooved?

Please let me know if any of this logic is flawed, i'm a bit of a newbie. I studied engineering at uni which mostly focused on differential equations. Since then i've been a Java developer and have become very interested in algorithm correctness.

Are there better ways to formally define an algorithm other that quantification and propositional logic?

It's definitely commendable that you're trying to come up with something for yourself here, but I'm afraid I can't quite understand what it is you have come up with. Since I'm a computer scientist, a working software developer and have a fairly broad knowledge of mathematics, this might indicate that there is a problem somewhere. In fact I think there are several problems:

1. Non-standard notation.

2. Confusing presentation.

3. How to define algorithms.

4. What it is you're proving.

Let's take those one by one.

1. Part of the problem is that your use of mathematical symbolism is quite non-standard. I'll let it pass that you're using "$=$" between Boolean conditions (though that will probably confuse a pure mathematicians; they tend to distinguish strictly between expressions and propositions), but it seems that you've gotten set builder notation the wrong way around. It should be $$\{ \langle\text{generic element}\rangle \mid \langle\text{conditions that each element must satisfy}\rangle \}$$ but it looks like you've switched the two sides of this notation around. I also suspect that you're using the wrong kind of quantifiers due to a misunderstanding of how the notation work. To pick a simpler example than the ones in your attempt, it looks like you would notate the set of all even integers as $$\tag{this is wrong!} \{ \forall x\in\mathbb Z\;(t=2x) \mid t \}$$ where the right notation would be $$\{ t \mid \exists x\in \mathbb Z\;(t=2x) \}$$ We using a $\exists$, because what the task of the condition is to tell us, when we have a suspected element already, whether that particular mathematical object is an element of the set or not. And the condition for some number $t$ to be even is that there is some whole number that multiplied by two yields $t$, not that every whole number multiplied by $2$ will yield $t$.

Actually, a more idiomatic way to write this would be just $$\{ 2x \mid x\in \mathbb Z \}$$ but never mind that.

Furthermore, you seem to be writing things like $t\in(t_1,t_2)$ when you mean that $t$ is an ordered pair of $t_1$ and $t_2$. There you should have used $=$ instead of $\in$ -- the thing to the right of an $\in$ is always a set.

Onwards to more weighty matters, though, --

2. It's hard to understand what you're trying to do, because you're never really explaining it, but rather jumping into symbols and formalism immediately. That can look "more mathematical" at the surface, but actually just makes it harder to understand. As a rule of thumb, each time you write a formula to introduce a new name or notation you will use later, you should also write some prose sentences that tell the reader how he should think about these things intuitively.

Don't shy away from English sentences! They are much better than formulas for communicating the gist of your argument. Use formulas only when it would be excessively clumsy to use words instead.

3. Finally we come to your real question: How to formalize reasoning about algorithms.

Actually, what one does in algorithm analysis is to talk about algorithms informally, using pseudocode! What you're writing here, even after making allowance for the strange symbolism, doesn't look like algorithms, it looks like a formal specification of what you'd like the algorithm to achieve -- but it's not an algorithm because it doesn't tell how to achieve it.

Since you're a Java developer, I assume you're comfortable enough with pseudocode itself, but is trying not to use it because you're afraid that it isn't mathematically "dignified" enough. But it's what the pros use, and it's much more readable and useful than trying to shoehorn it into formal logic notation.

If pseudocode is too informal, and we really want to speak formally about an algorithm, what is needed instead of pseudocode is actual code, that is, an implementation of the algorithm in a real programming language with a formal language specification. Very few people do formal reasoning about algorithms at that level. It happens in practice for some extremely high-risk projects such as software for spacecraft or safety-critical software for railway signaling or nuclear plant control. Programming-language researchers have been working to construct better tools for this for decades, but it is still not at a level where it is realistic to use in practical development.

Some styles of formal proofs about programs will of course use formal logic for expressing claims about the program -- but not to express the program itself.

4. What are you actually proving?

Your initial motivation said you were asked to make an algorithm more efficient, but from what I can see what you're actually attempting to prove is that two algorithms (really just two different descriptions of the problem) are equivalent.

You need to distinguish between two questions we can reason mathematically about:

1. Correctness: Does the algorithm actually produce the result we want it to produce?

2. Efficiency: How many resources (time, memory) does it need to run in different cases?

In your interview case, I imagine you must have been thinking of two different algorithms: One that has two nested loops through the list of numbers, trying all pairs to see if they have the right sum, and another one that starts by sorting the list and then moves pointers through it from both ends in lock-step until they meet.

Here we would ask first: Does the second algorithm do the right thing? It looks like this is what you're trying to argue in your question. However, unless in exceptional situations, an informal argument that it does would be more than sufficient.

What the interviewer was probably expecting you to consider was: Is the second algorithm more efficient than the first one? That is, is it faster? And if so, by how much?

There's a large and well-developed mathematical theory of algorithmic analysis that gives a precise way to answer such questions. It is too large for me to reproduce in an MSE answer, but basically the idea is to look at how much time each algorithm takes to run as a function of the length of the input list. Then we look at the asymptotic rate of growth of this function as the length of the input approaches infinity, and look for significant differences between the behavior of the algorithms, where "significant" means more than just a constant offset between the running times, or constant factors -- one algorithm always needing twice as much time as the other is "insignificant", whereas if the ration between the times needed the two algorithms get larger and larger as the input size grows, that's significant.

The results of this analysis is usually expressed in Big-O notation: The two-loop algorithm needs $O(n^2)$ time to process a list with $n$ elements, whereas the sort-then-loop-once algorithm needs $O(n\log n)$ time. Since $O(n\log n)$ grows slower than $O(n^2)$, the latter algorithm is better.

If you want to improve your knowledge about these matters (and I recommend that you do; many employers in the field care about this kind of knowledge), you should find yourself a textbook in analysis of algorithms and work through it. I don't know the market well enough to make concrete recommendations, though -- there are one or two out there with the exact title "Introduction to Algorithms", which can't be too far off, but I have no personal experience with them.

(... or if you're the type who accepts no imitations and wants to learn the real stuff the hard way, just get Knuth's The Art of Computer Programming and start on page 1 of vol. 1).

• +1 for this heroic effort to salvage what I thought was a doomed question! Apr 6, 2013 at 19:25
• Hello there, thanks for your detail reply, i'll be sure to get that notation right next time. Apr 6, 2013 at 19:42
• Knowing that programs are proofs I figured the ideally programs should be written as mathematical proofs. The more functional languages make this easier but writing the spec mathematically, which is effectively the program, is surely the way to go? en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence Apr 6, 2013 at 19:46
• @user1037729: The programs-as-proofs movement are actually going in the other direction: they want proofs that look like programs, not programs that look like proofs. Apr 6, 2013 at 20:46