Documentation

Mathlib.Data.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
    • Nondet.nil = { toMLList := MLList.nil }
    Instances For
      instance Nondet.instInhabitedNondet {σ : Type} {m : TypeType} [Lean.MonadBacktrack σ m] {α : Type} :
      Equations
      • Nondet.instInhabitedNondet = { default := Nondet.nil }
      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} {β : 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.instMonadNondet {σ : Type} {m : TypeType} [Monad m] [Lean.MonadBacktrack σ m] :

            Nondet m is a monad.

            Equations
            • Nondet.instMonadNondet = Monad.mk

            Nondet m is an alternative monad.

            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • Nondet.instMonadLiftNondet = { monadLift := fun {α : Type} => Nondet.singletonM }
            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
            • One or more equations did not get rendered due to their size.
            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} {β : 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} {β : 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} {β : 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} {β : 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} {β : 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