3 ms·
A proof that the quicksort algorithm terminates on all inputs
Testing my new language... This might be the slowest quicksort implementation yet, but hey, I didn't claim the code was optimal.
- paf31 16y agoTesting my new language, see http://typesandotherdistractions.com http://typesandotherdistractions.com
- mathgladiator 16y agoThat's very cool. Can you extend the type system such that functions are known to terminate? I've been curious about this since graduate school ( http://blog.mathgladiator.com/2011/03/research-problems-for-2011-and-beyond.html http://blog.mathgladiator.com/2011/03/research-problems-for-... ), and I've known for a while now that if you drop the turing machine capability, then you can build machines where halting is decidable. Does your language actually prove it halts, or more aptly, can you answer "Does it halt with either yes, no, unknown?"
- paf31 16y agoEverything involving only catamorphisms (|...|) terminates, since all atoms in the language define terminating functions, and least fixed point types can only be constructed in finite ways using the 'in' function or by catamorphism themselves, so are necessarily finite.
- paf31 16y agoYou may also be interested in Charity : http://pll.cpsc.ucalgary.ca/charity1/www/home.html http://pll.cpsc.ucalgary.ca/charity1/www/home.html - there is a similar quicksort algorithm on the Examples page.
- jderick 16y agoWhen I read proof, I assumed you meant you proved your quicksort returned an ordered permutation, but after looking at your webpage, I see you are only claiming to have proved termination. Not sure why you posted the github instead of your webpage, as without any explanation this code is nearly unintelligible. It would be interesting to hear an explanation of your example, it really is difficult to decipher. If you are interested in proving things about programs, you may want to check out some mechanical theorem provers such as ACL2, HOL or PVS.