A proof that the quicksort algorithm terminates on all inputs

https://gist.github.com/868615

by paf31 • 15 years ago

15 5 15 years ago

gist.github.com

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

paf313• 15 years ago

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

mathgladiator• 15 years ago

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?"

paf313• 15 years ago

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.

paf313• 15 years ago

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.

jderick• 15 years ago

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.

A proof that the quicksort algorithm terminates on all inputs

Related Stories