Hacker News Reader

Comment by kjeetgill | Hacker News Reader

I've always been intrigued by, but never delved deeply enough into the depths of the more mathematical sides of programming. I've always wondered is there a good mathematical representation of an algorithm that is useful for algebraic manipulation? For example:

Take an ugly equation like: x^2 + 3x+y+2+(−x)^2 = 3+(−x)^2 . It can be transformed to either (x+1)(x+2)-3 = y or y=−x^2−3x+1 fairly cleanly and usefully with just a few algebraic theorems. I remove redundancy among other things.

Can I take "bubble sort" work my way in steps to produce a "quick sort" or a "merge sort"? Sure you could prove they produce identical results but it doesn't feel like you're bridging that gap. Maybe this is too vague a question.

View on HN

The answer is surprisingly yes!

It's usually called equational reasoning or Bird–Meertens formalism.

Transforming an insertion sort into merge sort is covered in Section 5 of "FUNCTIONAL PEARLS The Third Homomorphism Theorem":

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45....

I can't begin to explain how excited I am to delve into this! Thank you for the lead.

You can have a look at Richard Bird's book _Pearls of Functional Algorithm Design_. It's much more accessible than his earlier influential book _Algebra of Programming_.

In this book, many well-known algorithms, e.g. KMP pattern matching, are derived from naive implementations by step-by-step applications of algebraic rules of (functional) programs.

Thanks!

Related to your last question, I was always puzzled by the following: when is a program an implementation of an (abstract) algorithm?

For example, can a program decide, given a sorting function implemented in language X, and an algorithm Y, whether or not the sorting function is an implementation of algorithm Y? Part of the question is how to represent algorithms (is "formal" pseudo-code the best way?)

Also, can you decide whether or not two functions written in different programming languages are implementations of the same algorithm?

> For example, can a program decide, given a sorting function implemented in language X, and an algorithm Y, whether or not the sorting function is an implementation of algorithm Y?

Assuming the usual things (e.g. that an algorithm Y can be specified in some useful, say, very high level language) then this problem is Halting-hard (e.g. at least as hard as the halting problem), because it would be showing the equivalence of two programs. A similar case applies to your latter question.

I'm not sure there's a good way of specifying abstract algorithms without running into this problem, but I'd be interested in defining a bit further what you might be thinking about.

Yes, in general it is obviously undecidable.

I should have been clearer, but I'm mostly interested in structure (traversal) algorithms, most of which could be coded in a language with bounded loops.

An easier question is the one of determining the complexity of an algorithm. I think there's a ton of work in this area, for example in techniques that use typing systems (types may for example specify how many times a parameter is used, thus allowing the program to infer the complexity).

(easier because the equivalence relation of "implementing the same algorithm" is strictly finer than "having the same complexity")

No you can't really, not that this has much to do with Curry-Howard.

Bubble sort and Quicksort only resemble each other in so much as the result is sorted. All of the other steps are completely different, meaning the abstract shapes of the intermediate computations are very different.

Reply on news.ycombinator.com