4 ms·

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 goo

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.

nilknarf 8y ago
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.2247&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45....
- kjeetgill 8y ago
  I can't begin to explain how excited I am to delve into this! Thank you for the lead.
  - yangzx 8y ago
    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.
    - kjeetgill 8y ago
      Thanks!
seanmcdirmid 8y ago
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.
gciruelos 8y ago
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?
- LolWolf 8y ago
  > 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.
  - gciruelos 8y ago
    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")

nilknarf 8y ago

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.2247&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.45....

kjeetgill 8y ago
I can't begin to explain how excited I am to delve into this! Thank you for the lead.
- yangzx 8y ago
  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.
  - kjeetgill 8y ago
    Thanks!

seanmcdirmid 8y ago

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.

gciruelos 8y ago

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?

LolWolf 8y ago
> 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.
- gciruelos 8y ago
  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")