Documentation

Batteries.Control.Nondet.Basic

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

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).

  • 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!

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

    The empty nondeterministic value.

    Equations
      Instances For
        instance Nondet.instInhabited {σ : Type} {m : TypeType} [Lean.MonadBacktrack σ m] {α : Type} :
        Equations
          def Nondet.squash {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (L : Unitm (Nondet m α)) :
          Nondet m α

          Squash a monadic nondeterministic value to a nondeterministic value.

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

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

              Equations
                Instances For
                  def Nondet.singleton {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] {α : Type} (x : α) :
                  Nondet m α

                  Convert a value to the singleton nondeterministic value.

                  Equations
                    Instances For
                      instance Nondet.instMonad {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] :

                      Nondet m is a monad.

                      Equations

                        Nondet m is an alternative monad.

                        Equations
                          instance Nondet.instMonadLift {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] :
                          Equations
                            def Nondet.ofListM {σ : Type} {m : TypeType} [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
                              Instances For
                                def Nondet.ofList {σ : Type} {m : TypeType} [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
                                  Instances For
                                    def Nondet.mapM {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] {α β : 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
                                      Instances For
                                        def Nondet.map {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] {α β : Type} (f : αβ) (L : Nondet m α) :
                                        Nondet m β

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

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

                                            Convert a monadic optional value to a nondeterministic value.

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

                                                Convert an optional value to a nondeterministic value.

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

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

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

                                                        Filter and map a nondeterministic value.

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

                                                            Filter a nondeterministic value using a monadic predicate.

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

                                                                Filter a nondeterministic value.

                                                                Equations
                                                                  Instances For
                                                                    partial def Nondet.iterate {σ : Type} {m : TypeType} [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 : TypeType} [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
                                                                      Instances For
                                                                        def Nondet.firstM {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] {α β : 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
                                                                          Instances For
                                                                            def Nondet.toMLList' {σ : Type} {m : TypeType} [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
                                                                              Instances For
                                                                                def Nondet.toList {σ : Type} {m : TypeType} [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
                                                                                  Instances For
                                                                                    def Nondet.toList' {σ : Type} {m : TypeType} [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
                                                                                      Instances For

                                                                                        The Id monad is trivially backtrackable, with state Unit.

                                                                                        Equations