Appropriate nondeterminism monad

Stream: new members

[Simeon Duwel]

Hi all,

I'm having trouble implementing a nondeterministic search algorithm. For context, you can refer to this earlier post where I explain what I'm trying to do, or my new repository.

Concretely, the following algorithm works, but crashes on relatively small input sizes:

def mkTree' {len: Nat} (pOrder: POrder len) (depth: Nat := maxDepth len) : Many (SortingTree len) :=
  match pOrder.incompPairs with
    | [] => Many.one $ SortingTree.Leaf pOrder.toOrder
    | ps => match depth with
      | 0 => Many.none
      | depth' + 1 => Many.fromList ps >>= λ p ↦ do
        let lt ← mkTree' (pOrder.add p) depth';
        let gt ← mkTree' (pOrder.add p.swap) depth';
        pure $ SortingTree.Branch p lt gt

and this is the only way I see to write this algorithm.

Is there a more suitable nondeterminism monad than the one described in Functional Programming With Lean's chapter on monads? I tried using MLList Thunk to little avail (I blew through stack space way too quickly anyway) and Nondet Id from Batteries ; but I think I don't know enough about how that works concretely to have implemented it correctly. Any pointers would be nice.

[Aaron Liu]

I think what you want is a depth-first search

[Simeon Duwel]

yes, I agree, and I thought Nondet's iterate method looked promising, but I'm feeling quite lost tbh...

[Aaron Liu]

Why not just write a depth-first search - have a stack State that you append to each time you search and pop from each time you backtrack

[Aaron Liu]

Make sure to make it tail recursive

[Simeon Duwel]

Wait State as in the state monad?

[Simeon Duwel]

or a custom State structure that holds the necessary information to backtrack

[Aaron Liu]

Your choice