|
I found this paper via the recent discussion about point free style. I found the paper quite enjoyable and interesting so I wanted to point it out to other LtU readers.
Aside from discussing how using point free style can help with proofs, this paper is a nice example of program transformation. The author shows how you can prove the correctness of radix sort by mechanically transforming a more intuitive sorting algorithm into an implementation of radix sort.
Personally, I find radix sort quite intuitive. Convincing myself that the code for treesort in the paper is correct was slightly harder than grasping and proving why radix sort works, so perhaps in this respect this example isn't ideal for showing the importance of program transformation as a proof technique.
Still this is a nice example, well worth playing with if you like Haskell.
Notice that the code in appedix B can be useful for playing with the sorting code presented earlier in the paper.
Posted to functional by Ehud Lamm on 7/1/03; 6:45:47 AM
|
A Pointless Derivation of Radixsort
