Skip to content

Adding monadic fixpoint to define Mu's quicksort #26

@t6s

Description

@t6s

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions