a blog about things that I've been thinking hard about

The "Essence" of an Algorithm and Equational Reasoning

12 April, 2012
by Philip Dorrell

What is an algorithm?

Wikipedia tells me an algorithm "is a step-by-step procedure for calculations".

A related question is: "When are two algorithms the same?". Actually, I think that is an important part of the first question. To say what an algorithm is, is to say what one algorithm is, as opposed to, say, two algorithms.

One paper that asks exactly this question is When are two algorithms the same ?

Algorithms and Proofs

Actually, this is not the first time I have asked What is an Algorithm?

In that earlier article I suggested that an "algorithm" is the thing that gets re-used when you write yet another implementation of that algorithm in some particular language. And that the one thing that is truly reusable is not program code of any sort, but mathematical proofs.

So I partly identified an "algorithm" with the mathematical proof of its correctness.

Equational Proofs

In this article, I am going to explore this idea further, and consider equational proofs.

Equational reasoning is a style of reasoning where all axioms are stated as equalities, and all proof steps occur via variations of substitution.

Euclid's Algorithm

The "Hello World" of "what is an algorithm" analyses seems to be Euclid's Algorithm.

Here is an implementation of Euclid's Algorithm in Ruby:

def gcd(x, y)
  while y != 0 do
    new_x = y
    y = x % y
    x = new_x
  end
  x
end

As many people have observed, the problem with programming variables, is that a statement like

a = a + 1

doesn't make sense. Like, surely a is never equal to a+1!

There are various ways to deal with this problem. One is just to tell people to forget all about algebra when they start programming. Another is to insist on using functional programming, where no variable ever has its value set more than once.

Yet another approach is to realise that the a on the left hand side and the a on the right hand side are different variables, and that if we want to do algebra with them, we should given them different names. Like:

a2 = a1 + 1

We can do something similar with the GCD code above. For example, there are two different assignments to a variable x:

  1. The initial assignment to the in-parameter.
  2. The assignment x = new_x.

And similarly two assignments to the variable y.

But that doesn't quite solve the "multiple assignment" problem, because the code also contains a loop, and each time the loop goes round, there is a new occurrence of each assignment in the loop.

The only way to avoid those multiple assignments is to index each variable, as well as differentiating other re-occurrences of assignment to the same variable. For an index, we need a loop counter, which is simply a count of how many times we have been around the loop. Putting all of that together, we get a program something like this:

def gcd(x_param, y_param)
  x(0)=x_param
  y(0)=y_param
  condition(0) = y(0) != 0
  counter = 0
  while (condition(counter)) do
    new_x(counter) = y(counter)
    y_2(counter) = x(counter) % y(counter)
    x_2(counter) = new_x(counter)
    x(counter+1) = x_2(counter)
    y(counter+1) = y_2(counter)
    condition(counter+1) = y(counter+1) != 0
    counter++
  end
  condition(counter_max) = false
  result = x(counter_max)
end

We could add some initial assumptions, that the parameters x and y are both positive integers:


x ϵ 𝕀
y ϵ 𝕀
x > 0
y > 0

def gcd(x_param, y_param)
  x_param ϵ 𝕀
  y_param ϵ 𝕀
  x_param > 0
  y_param > 0
  x(0)=x_param
  y(0)=y_param
  condition(0) = y(0) != 0
  counter = 0
  while (condition(counter)) do
    condition(counter) = true
    new_x(counter) = y(counter)
    y_2(counter) = x(counter) % y(counter)
    x_2(counter) = new_x(counter)
    x(counter+1) = x_2(counter)
    y(counter+1) = y_2(counter)
    condition(counter+1) = y(counter+1) != 0
    counter++
  end
  condition(counter_max) = false
  result = x(counter_max)
end

At this point, almost everything in the code has been compiled into equations and other predicates. The only exception is the structure of the while loop, and the counter variable associated with it. counter_max represents the maximum value of counter, after the loop terminates. Of course we have to prove that the loop does terminate before we can treat any statements about counter_max as theorems.

We can now consider some lemmas, which we will use to prove the correctness of the algorithm:

(Assuming in all cases that x and y are integers. Also note that GCD in capitals represents the mathematical function GCD, distinct from the lower-case gcd which is the name of the code function being defined and analysed.)

 x ϵ 𝕀 and y ϵ 𝕀 => x%y ϵ 𝕀
 x >= 0 and y > 0 => x % y >= 0
 x >=0 and y > 0 => GCD(x%y) = GCD(x,y)
 GCD(x,y) = GCD(y,x)
 x >= 0 and y > 0 and x > y => x%y < y
 x > 0 => GCD(x,0) = x

Applying these lemmas, we can straightforwardly prove various theorems:


x ϵ 𝕀
y ϵ 𝕀
x > 0
y > 0

def gcd(x_param, y_param)
  x_param ϵ 𝕀
  y_param ϵ 𝕀
  x_param > 0
  y_param > 0
  x(0)=x_param
  y(0)=y_param
  x(0) ϵ 𝕀
  y(0) ϵ 𝕀
  x(0) >= 0
  y(0) > 0
  condition(0) = y(0) != 0
  counter = 0
  while (condition(counter)) do
    condition(counter) = true
    y(counter) != 0
    
    new_x(counter) = y(counter)
    y_2(counter) = x(counter) % y(counter)
    GCD(y_2(counter),y(counter)) = GCD(x(counter),y(counter))
    x_2(counter) = new_x(counter)
    x(counter+1) = x_2(counter)
    y(counter+1) = y_2(counter)
    GCD(x(counter+1),y(counter+1)) = GCD(x_2(counter),y_2(counter))
    condition(counter+1) = y(counter+1) != 0
    counter++
  end
  condition(counter_max) = false
  result = x(counter_max)
end
Vote for or comment on this article on Reddit or Hacker News ...