A proof that the quicksort algorithm terminates on all inputs

gist.github.com

15 points·paf31··5 comments

Testing my new language... This might be the slowest quicksort implementation yet, but hey, I didn't claim the code was optimal.

Open articleView on HN

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

That'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-... ), 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?"

Testing my new language, see http://typesandotherdistractions.com

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

You may also be interested in Charity : http://pll.cpsc.ucalgary.ca/charity1/www/home.html - there is a similar quicksort algorithm on the Examples page.

Reply on news.ycombinator.com