monae icon indicating copy to clipboard operation
monae copied to clipboard

Adding monadic fixpoint to define Mu's quicksort

Open t6s opened this issue 4 years ago • 0 comments

The definition of qperm function in the quicksort branch requires an interaction between fixpoints and binds to show its termination. Currently there is no such mechanism, and it seems hard to finish the definition.

One possible solution is in http://leventerkok.github.io/papers/mfix.pdf : the monadic fixpoint operator mfix. Let's see if this mfix can be added to monae with useful laws and if this enables quicksort.

t6s avatar Sep 16 '20 01:09 t6s