Query costs of decision trees

weightedCost charges each query made on an input, including repeated queries. weightedDepth is the largest cost of a structural root-to-leaf path. It bounds the actual cost, but equality need not hold: repeated variables can make a structural path unreachable. Costs are natural numbers and may be zero. Unit costs give the actual query count cost and the usual depth.

These quantities support composition when different queried bits have different computation costs; no second notion of minimum decision-tree complexity is introduced.

Main definitions

• Cslib.DecisionTree.weightedCost: the cost of the queries executed on one input.
• Cslib.DecisionTree.cost: the number of queries executed on one input.
• Cslib.DecisionTree.weightedDepth: the maximum structural path cost.

Main results

• Cslib.DecisionTree.weightedCost_le_weightedDepth: structural cost bounds actual cost.
• Cslib.DecisionTree.weightedDepth_le_depth_mul: a uniform query bound gives a depth bound.

def Cslib.DecisionTree.weightedCost {ι : Type u_1} {β : Type u_3} : DecisionTree ι β → (ι → ℕ) → (ι → Bool) → ℕ

The total cost of queries executed on an input, counting repeated queries each time.

def Cslib.DecisionTree.cost {ι : Type u_1} {β : Type u_3} (t : DecisionTree ι β) (x : ι → Bool) : ℕ

The number of queries executed on an input, including repeated queries.

def Cslib.DecisionTree.weightedDepth {ι : Type u_1} {β : Type u_3} : DecisionTree ι β → (ι → ℕ) → ℕ

The maximum cost of a structural root-to-leaf path, including unreachable paths.

@[simp]

theorem Cslib.DecisionTree.weightedCost_leaf {ι : Type u_1} {β : Type u_3} (b : β) (w : ι → ℕ) (x : ι → Bool) : (leaf b).weightedCost w x = 0

@[simp]

theorem Cslib.DecisionTree.weightedCost_node {ι : Type u_1} {β : Type u_3} (i : ι) (left right : DecisionTree ι β) (w : ι → ℕ) (x : ι → Bool) : (node i left right).weightedCost w x = (bif x i then right.weightedCost w x else left.weightedCost w x) + w i

@[simp]

theorem Cslib.DecisionTree.cost_leaf {ι : Type u_1} {β : Type u_3} (b : β) (x : ι → Bool) : (leaf b).cost x = 0

@[simp]

theorem Cslib.DecisionTree.cost_node {ι : Type u_1} {β : Type u_3} (i : ι) (left right : DecisionTree ι β) (x : ι → Bool) : (node i left right).cost x = (bif x i then right.cost x else left.cost x) + 1

@[simp]

theorem Cslib.DecisionTree.weightedDepth_leaf {ι : Type u_1} {β : Type u_3} (b : β) (w : ι → ℕ) : (leaf b).weightedDepth w = 0

@[simp]

theorem Cslib.DecisionTree.weightedDepth_node {ι : Type u_1} {β : Type u_3} (i : ι) (left right : DecisionTree ι β) (w : ι → ℕ) : (node i left right).weightedDepth w = max (left.weightedDepth w) (right.weightedDepth w) + w i

theorem Cslib.DecisionTree.weightedDepth_mono {ι : Type u_1} {β : Type u_3} (t : DecisionTree ι β) {w v : ι → ℕ} (h : ∀ (i : ι), w i ≤ v i) : t.weightedDepth w ≤ t.weightedDepth v

Increasing query costs cannot decrease structural path cost.

@[simp]

theorem Cslib.DecisionTree.weightedDepth_const {ι : Type u_1} {β : Type u_3} (t : DecisionTree ι β) (c : ℕ) : (t.weightedDepth fun (x : ι) => c) = t.depth * c

A constant query cost multiplies the ordinary structural depth.

theorem Cslib.DecisionTree.weightedDepth_le_depth_mul {ι : Type u_1} {β : Type u_3} (t : DecisionTree ι β) {w : ι → ℕ} {d : ℕ} (h : ∀ (i : ι), w i ≤ d) : t.weightedDepth w ≤ t.depth * d

Charging at most d per query costs at most depth * d on every structural path.

theorem Cslib.DecisionTree.weightedCost_le_weightedDepth {ι : Type u_1} {β : Type u_3} (t : DecisionTree ι β) (w : ι → ℕ) (x : ι → Bool) : t.weightedCost w x ≤ t.weightedDepth w

The actual path cost is bounded by the largest structural path cost.

theorem Cslib.DecisionTree.cost_le_depth {ι : Type u_1} {β : Type u_3} (t : DecisionTree ι β) (x : ι → Bool) : t.cost x ≤ t.depth

The number of queries executed on any input is at most the structural depth.

@[simp]

theorem Cslib.DecisionTree.weightedDepth_mapQueries {ι : Type u_1} {κ : Type u_2} {β : Type u_3} (f : ι → κ) (t : DecisionTree ι β) (w : κ → ℕ) : (mapQueries f t).weightedDepth w = t.weightedDepth (w ∘ f)

Relabelling queries pulls their costs back along the relabelling function.

@[simp]

theorem Cslib.DecisionTree.weightedCost_mapQueries {ι : Type u_1} {κ : Type u_2} {β : Type u_3} (f : ι → κ) (t : DecisionTree ι β) (w : κ → ℕ) (x : κ → Bool) : (mapQueries f t).weightedCost w x = t.weightedCost (w ∘ f) (x ∘ f)

Relabelling queries pulls back both the oracle and its query costs.