# Documentation

Mathlib.Data.Nondet.Basic

We represent nondeterministic values in a type α as a single field structure containing an MLList m (σ × α), i.e. as a monadic lazy list of possible values, each equipped with the backtrackable state required to run further computations in the ambient monad.

We provide an Alternative Monad instance, as well as functions bind, mapM, and filterMapM, and functions singletonM, ofListM, ofOptionM, and firstM for entering and leaving the nondeterministic world.

Operations on the nondeterministic value via bind, mapM, and filterMapM run with the appropriate backtrackable state, and are responsible for updating the state themselves (typically this doesn't need to be done explicitly, but just happens as a side effect in the monad m).

structure Nondet {σ : Type} (m : ) [] (α : Type) :
• toMLList : MLList m (α × σ)

Convert a non-deterministic value into a lazy list, keeping the backtrackable state. Be careful that monadic operations on the MLList will not respect this state!

Nondet m α is variation on MLList m α suitable for use with backtrackable monads m.

We think of Nondet m α as a nondeterministic value in α, with the possible alternatives stored in a monadic lazy list.

Along with each a : α we store the backtrackable state, and ensure that monadic operations on alternatives run with the appropriate state.

Operations on the nondeterministic value via bind, mapM, and filterMapM run with the appropriate backtrackable state, and are responsible for updating the state themselves (typically this doesn't need to be done explicitly, but just happens as a side effect in the monad m).

Instances For
def Nondet.nil {σ : Type} {m : } [] {α : Type} :
Nondet m α

The empty nondeterministic value.

Instances For
instance Nondet.instInhabitedNondet {σ : Type} {m : } [] {α : Type} :
def Nondet.squash {σ : Type} {m : } [] [] {α : Type} (L : Unitm (Nondet m α)) :
Nondet m α

Squash a monadic nondeterministic value to a nondeterministic value.

Instances For
partial def Nondet.bind {σ : Type} {m : } [] [] {α : Type} {β : Type} (L : Nondet m α) (f : αNondet m β) :
Nondet m β

Bind a nondeterministic function over a nondeterministic value, ensuring the function is run with the relevant backtrackable state at each value.

def Nondet.singletonM {σ : Type} {m : } [] [] {α : Type} (x : m α) :
Nondet m α

Convert any value in the monad to the singleton nondeterministic value.

Instances For
def Nondet.singleton {σ : Type} {m : } [] [] {α : Type} (x : α) :
Nondet m α

Convert a value to the singleton nondeterministic value.

Instances For
instance Nondet.instMonadNondet {σ : Type} {m : } [] [] :

Nondet m is a monad.

instance Nondet.instAlternativeNondet {σ : Type} {m : } [] [] :

Nondet m is an alternative monad.

instance Nondet.instMonadLiftNondet {σ : Type} {m : } [] [] :
def Nondet.ofListM {σ : Type} {m : } [] [] {α : Type} (L : List (m α)) :
Nondet m α

Lift a list of monadic values to a nondeterministic value. We ensure that each monadic value is evaluated with the same backtrackable state.

Instances For
def Nondet.ofList {σ : Type} {m : } [] [] {α : Type} (L : List α) :
Nondet m α

Lift a list of values to a nondeterministic value. (The backtrackable state in each will be identical: whatever the state was when we first read from the result.)

Instances For
def Nondet.mapM {σ : Type} {m : } [] [] {α : Type} {β : Type} (f : αm β) (L : Nondet m α) :
Nondet m β

Apply a function which returns values in the monad to every alternative of a Nondet m α.

Instances For
def Nondet.map {σ : Type} {m : } [] [] {α : Type} {β : Type} (f : αβ) (L : Nondet m α) :
Nondet m β

Apply a function to each alternative in a Nondet m α .

Instances For
def Nondet.ofOptionM {σ : Type} {m : } [] [] {α : Type} (x : m ()) :
Nondet m α

Convert a monadic optional value to a nondeterministic value.

Instances For
def Nondet.ofOption {σ : Type} {m : } [] [] {α : Type} (x : ) :
Nondet m α

Convert an optional value to a nondeterministic value.

Instances For
def Nondet.filterMapM {σ : Type} {m : } [] [] {α : Type} {β : Type} (f : αm ()) (L : Nondet m α) :
Nondet m β

Filter and map a nondeterministic value using a monadic function which may return none.

Instances For
def Nondet.filterMap {σ : Type} {m : } [] [] {α : Type} {β : Type} (f : α) (L : Nondet m α) :
Nondet m β

Filter and map a nondeterministic value.

Instances For
def Nondet.filterM {σ : Type} {m : } [] [] {α : Type} (p : αm ()) (L : Nondet m α) :
Nondet m α

Filter a nondeterministic value using a monadic predicate.

Instances For
def Nondet.filter {σ : Type} {m : } [] [] {α : Type} (p : αBool) (L : Nondet m α) :
Nondet m α

Filter a nondeterministic value.

Instances For
partial def Nondet.iterate {σ : Type} {m : } [] [] {α : Type} (f : αNondet m α) (a : α) :
Nondet m α

All iterations of a non-deterministic function on an initial value.

(That is, depth first search.)

def Nondet.head {σ : Type} {m : } [] [] {α : Type} [] (L : Nondet m α) :
m α

Find the first alternative in a nondeterministic value, as a monadic value.

Instances For
def Nondet.firstM {σ : Type} {m : } [] [] {α : Type} {β : Type} [] (L : Nondet m α) (f : αm ()) :
m β

Find the value of a monadic function on the first alternative in a nondeterministic value where the function succeeds.

Instances For
def Nondet.toMLList' {σ : Type} {m : } [] [] {α : Type} (L : Nondet m α) :
MLList m α

Convert a non-deterministic value into a lazy list, by discarding the backtrackable state.

Instances For
def Nondet.toList {σ : Type} {m : } [] [] {α : Type} (L : Nondet m α) :
m (List (α × σ))

Convert a non-deterministic value into a list in the monad, retaining the backtrackable state.

Instances For
def Nondet.toList' {σ : Type} {m : } [] [] {α : Type} (L : Nondet m α) :
m (List α)

Convert a non-deterministic value into a list in the monad, by discarding the backtrackable state.

Instances For

The Id monad is trivially backtrackable, with state Unit.