Hacker News Reader

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....

View on HN

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!

Reply on news.ycombinator.com