Documentation

Complexitylib.Circuits.DecisionTree.Finite.Defs

Finite-arity decision trees -- definitions #

The original DecisionTree syntax uses natural-number query labels. Switching arguments, however, count restrictions on exactly N variables. DecisionTree.On N makes that arity part of the type and prevents out-of-range queries.

source
inductive Complexity.DecisionTree.On (N : ℕ) :
Type

A Boolean decision tree whose every query is one of exactly N variables.

  • leaf {N : ℕ} (value : Bool) : On N

    A leaf carrying its Boolean output.

  • node {N : ℕ} (index : Fin N) (ifFalse ifTrue : On N) : On N

    Query index, taking ifFalse on zero and ifTrue on one.

Instances For
    source
    @[implicit_reducible]
    instance Complexity.DecisionTree.instReprOn {N✝ : ℕ} :
    Repr (On N✝)
    Equations
    source
    def Complexity.DecisionTree.instReprOn.repr {N✝ : ℕ} :
    On N✝ → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.DecisionTree.instDecidableEqOn.decEq {N✝ : ℕ} (x✝ x✝¹ : On N✝) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Complexity.DecisionTree.instDecidableEqOn {N✝ : ℕ} :
        DecidableEq (On N✝)
        Equations
        source
        def Complexity.DecisionTree.On.eval {N : ℕ} (input : BitString N) :
        On N → Bool

        Evaluate a finite-arity decision tree.

        Equations
        Instances For
          source
          def Complexity.DecisionTree.On.depth {N : ℕ} :
          On N → ℕ

          Maximum number of queries on any root-to-leaf path.

          Equations
          Instances For
            source
            def Complexity.DecisionTree.On.numLeaves {N : ℕ} :
            On N → ℕ

            Number of leaves.

            Equations
            Instances For
              source
              def Complexity.DecisionTree.On.vars {N : ℕ} :
              On N → Finset (Fin N)

              The finite set of variables queried by the tree.

              Equations
              Instances For
                source
                def Complexity.DecisionTree.On.neg {N : ℕ} :
                On N → On N

                Negate a decision tree by complementing every leaf.

                Equations
                Instances For
                  source
                  def Complexity.DecisionTree.On.toDecisionTree {N : ℕ} :
                  On N → DecisionTree

                  Erase the arity proof from every query label.

                  Equations
                  Instances For
                    source
                    def Complexity.DecisionTree.On.restrict {N : ℕ} (restriction : Restriction.On N) :
                    On N → On N

                    Simplify a finite decision tree under a matching restriction.

                    Equations
                    Instances For