A nondeterminism monad.

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 → Type) [Lean.MonadBacktrack σ m] (α : Type) : 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).

def Nondet.nil {σ : Type} {m : Type → Type} [Lean.MonadBacktrack σ m] {α : Type} : Nondet m α

The empty nondeterministic value.

Equations

• Nondet.nil = { toMLList := MLList.nil }

instance Nondet.instInhabitedNondet {σ : Type} {m : Type → Type} [Lean.MonadBacktrack σ m] {α : Type} : Inhabited (Nondet m α)

Equations

• Nondet.instInhabitedNondet = { default := Nondet.nil }

def Nondet.squash {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Unit → m (Nondet m α)) : Nondet m α

Squash a monadic nondeterministic value to a nondeterministic value.

Equations

• Nondet.squash L = { toMLList := MLList.squash fun x => do let __do_lift ← L () pure __do_lift.toMLList }

partial def Nondet.bind {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ 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 → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : m α) : Nondet m α

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

Equations

• Nondet.singletonM x = { toMLList := MLList.singletonM do let a ← x let __do_lift ← Lean.saveState pure (a, __do_lift) }

def Nondet.singleton {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : α) : Nondet m α

Convert a value to the singleton nondeterministic value.

Equations

• Nondet.singleton x = Nondet.singletonM (pure x)

instance Nondet.instMonadNondet {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] : Monad (Nondet m)

Nondet m is a monad.

Equations

• Nondet.instMonadNondet = Monad.mk

instance Nondet.instAlternativeNondet {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] : Alternative (Nondet m)

Nondet m is an alternative monad.

Equations

• Nondet.instAlternativeNondet = Alternative.mk (fun {α} => Nondet.nil) fun {α} x y => { toMLList := MLList.append x.toMLList fun x => (y ()).toMLList }

instance Nondet.instMonadLiftNondet {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] : MonadLift m (Nondet m)

Equations

• Nondet.instMonadLiftNondet = { monadLift := fun {α} => Nondet.singletonM }

def Nondet.ofListM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ 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.

Equations

• One or more equations did not get rendered due to their size.

def Nondet.ofList {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ 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.)

Equations

• Nondet.ofList L = Nondet.ofListM (List.map pure L)

def Nondet.mapM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ 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 α.

Equations

• Nondet.mapM f L = Nondet.bind L fun a => Nondet.singletonM (f a)

def Nondet.map {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → β) (L : Nondet m α) : Nondet m β

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

Equations

• Nondet.map f L = Nondet.mapM (fun a => pure (f a)) L

def Nondet.ofOptionM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : m (Option α)) : Nondet m α

Convert a monadic optional value to a nondeterministic value.

Equations

• Nondet.ofOptionM x = Nondet.squash fun x => do let __do_lift ← x match __do_lift with | none => pure Nondet.nil | some a => pure (Nondet.singleton a)

def Nondet.ofOption {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : Option α) : Nondet m α

Convert an optional value to a nondeterministic value.

Equations

• Nondet.ofOption x = Nondet.ofOptionM (pure x)

def Nondet.filterMapM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → m (Option β)) (L : Nondet m α) : Nondet m β

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

Equations

• Nondet.filterMapM f L = Nondet.bind L fun a => Nondet.ofOptionM (f a)

def Nondet.filterMap {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} (f : α → Option β) (L : Nondet m α) : Nondet m β

Filter and map a nondeterministic value.

Equations

• Nondet.filterMap f L = Nondet.filterMapM (fun a => pure (f a)) L

def Nondet.filterM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (p : α → m (ULift Bool)) (L : Nondet m α) : Nondet m α

Filter a nondeterministic value using a monadic predicate.

Equations

• Nondet.filterM p L = Nondet.filterMapM (fun a => do let __do_lift ← p a if __do_lift.down = true then pure (some a) else pure none) L

def Nondet.filter {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (p : α → Bool) (L : Nondet m α) : Nondet m α

Filter a nondeterministic value.

Equations

• Nondet.filter p L = Nondet.filterM (fun a => pure { down := p a }) L

partial def Nondet.iterate {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ 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 → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} [Alternative m] (L : Nondet m α) : m α

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

Equations

• Nondet.head L = do let __discr ← MLList.head L.toMLList match __discr with | (x, s) => do Lean.restoreState s pure x

def Nondet.firstM {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} {β : Type} [Alternative m] (L : Nondet m α) (f : α → m (Option β)) : m β

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

Equations

• Nondet.firstM L f = Nondet.head (Nondet.filterMapM f L)

def Nondet.toMLList' {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Nondet m α) : MLList m α

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

Equations

• Nondet.toMLList' L = MLList.map (fun x => x.fst) L.toMLList

def Nondet.toList {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Nondet m α) : m (List (α × σ))

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

Equations

• Nondet.toList L = MLList.force L.toMLList

def Nondet.toList' {σ : Type} {m : Type → Type} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Nondet m α) : m (List α)

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

Equations

• Nondet.toList' L = MLList.force (MLList.map (fun x => x.fst) L.toMLList)

instance instMonadBacktrackUnitId : Lean.MonadBacktrack Unit Id

The Id monad is trivially backtrackable, with state Unit.

Equations

• instMonadBacktrackUnitId = { saveState := pure (), restoreState := fun x => pure () }