Composition of decision trees

bind replaces each output leaf by a continuation. substitute replaces each query by a Boolean-valued decision tree and continues according to its answer. These are executable tree constructions, with exact evaluation and per-input cost laws. The input variables of different subroutines may overlap, and repeated queries are charged each time; substitution does not cache their answers.

The structural cost of substitution is bounded by the outer tree's weighted depth, charging each query the inner tree's structural cost. This is generally sharper than multiplying by the most expensive query. Minimizing over trees gives the usual deterministic composition upper bound. The disjoint-block corollary allows a different finite coordinate type for every block, including empty blocks. No multiplicative lower bound is asserted.

Main definitions

• Cslib.DecisionTree.bind: replace output leaves by continuations.
• Cslib.DecisionTree.substitute: replace queries by Boolean-valued subroutines.

Main results

• Cslib.DecisionTree.eval_substitute: query substitution computes function composition.
• Cslib.DecisionTree.weightedCost_substitute: exact input-dependent composition cost.
• Cslib.DecisionTree.weightedDepth_substitute_le: composition with heterogeneous query costs.
• Cslib.DecisionTree.complexity_substitute_le: a weighted bound using any outer decision tree.
• Cslib.DecisionTree.complexity_substitute_le_mul: the uniform shared-input composition bound.
• Cslib.DecisionTree.complexity_blockCompose_le_mul: the disjoint-block composition bound.

def Cslib.DecisionTree.bind {ι : Type u_1} {β : Type u_4} {γ : Type u_5} : DecisionTree ι β → (β → DecisionTree ι γ) → DecisionTree ι γ

Replace each leaf labelled b by the continuation k b.

@[simp]

theorem Cslib.DecisionTree.leaf_bind {ι : Type u_1} {β : Type u_4} {γ : Type u_5} (b : β) (k : β → DecisionTree ι γ) : (leaf b).bind k = k b

@[simp]

theorem Cslib.DecisionTree.node_bind {ι : Type u_1} {β : Type u_4} {γ : Type u_5} (i : ι) (left right : DecisionTree ι β) (k : β → DecisionTree ι γ) : (node i left right).bind k = node i (left.bind k) (right.bind k)

@[simp]

theorem Cslib.DecisionTree.bind_leaf {ι : Type u_1} {β : Type u_4} (t : DecisionTree ι β) : t.bind leaf = t

Replacing each leaf by itself preserves the tree.

theorem Cslib.DecisionTree.bind_assoc {ι : Type u_1} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} (t : DecisionTree ι β) (k : β → DecisionTree ι γ) (l : γ → DecisionTree ι δ) : (t.bind k).bind l = t.bind fun (b : β) => (k b).bind l

Successive leaf substitutions associate.

@[simp]

theorem Cslib.DecisionTree.eval_bind {ι : Type u_1} {β : Type u_4} {γ : Type u_5} (t : DecisionTree ι β) (k : β → DecisionTree ι γ) (x : ι → Bool) : (t.bind k).eval x = (k (t.eval x)).eval x

Evaluate the first tree, then its selected continuation on the same input.

theorem Cslib.DecisionTree.weightedCost_bind {ι : Type u_1} {β : Type u_4} {γ : Type u_5} (t : DecisionTree ι β) (k : β → DecisionTree ι γ) (w : ι → ℕ) (x : ι → Bool) : (t.bind k).weightedCost w x = t.weightedCost w x + (k (t.eval x)).weightedCost w x

Leaf substitution adds exactly the costs of the two executed computations.

theorem Cslib.DecisionTree.weightedDepth_bind_le {ι : Type u_1} {β : Type u_4} {γ : Type u_5} (t : DecisionTree ι β) (k : β → DecisionTree ι γ) (w : ι → ℕ) {d : ℕ} (hk : ∀ (b : β), (k b).weightedDepth w ≤ d) : (t.bind k).weightedDepth w ≤ t.weightedDepth w + d

A uniform bound on continuation costs adds to the first tree's structural cost.

theorem Cslib.DecisionTree.depth_bind_le {ι : Type u_1} {β : Type u_4} {γ : Type u_5} (t : DecisionTree ι β) (k : β → DecisionTree ι γ) {d : ℕ} (hk : ∀ (b : β), (k b).depth ≤ d) : (t.bind k).depth ≤ t.depth + d

A uniform bound on continuation depths adds to the first tree's depth.

def Cslib.DecisionTree.substitute {ι : Type u_1} {κ : Type u_2} {β : Type u_4} : DecisionTree ι β → (ι → DecisionTree κ Bool) → DecisionTree κ β

Replace a query of i by the Boolean subroutine s i, then follow its answer. Every occurrence is replaced independently; answers are not memoized.

@[simp]

theorem Cslib.DecisionTree.substitute_leaf {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (b : β) (s : ι → DecisionTree κ Bool) : (leaf b).substitute s = leaf b

theorem Cslib.DecisionTree.substitute_node {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (i : ι) (left right : DecisionTree ι β) (s : ι → DecisionTree κ Bool) : (node i left right).substitute s = (s i).bind fun (b : Bool) => bif b then right.substitute s else left.substitute s

@[simp]

theorem Cslib.DecisionTree.substitute_mapQueries {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (t : DecisionTree ι β) (f : ι → κ) : (t.substitute fun (i : ι) => node (f i) (leaf false) (leaf true)) = mapQueries f t

Replacing queries by single-query trees is ordinary query relabelling.

theorem Cslib.DecisionTree.substitute_bind {ι : Type u_1} {κ : Type u_2} {β : Type u_4} {γ : Type u_5} (t : DecisionTree ι β) (k : β → DecisionTree ι γ) (s : ι → DecisionTree κ Bool) : (t.bind k).substitute s = (t.substitute s).bind fun (b : β) => (k b).substitute s

Query substitution distributes over leaf substitution.

theorem Cslib.DecisionTree.substitute_assoc {ι : Type u_1} {κ : Type u_2} {μ : Type u_3} {β : Type u_4} (t : DecisionTree ι β) (s : ι → DecisionTree κ Bool) (r : κ → DecisionTree μ Bool) : (t.substitute s).substitute r = t.substitute fun (i : ι) => (s i).substitute r

Nested query substitutions associate, so subroutines may be compiled in stages.

@[simp]

theorem Cslib.DecisionTree.eval_substitute {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (t : DecisionTree ι β) (s : ι → DecisionTree κ Bool) (x : κ → Bool) : (t.substitute s).eval x = t.eval fun (i : ι) => (s i).eval x

Query substitution evaluates the outer tree on the answers supplied by the inner trees.

theorem Cslib.DecisionTree.Computes.substitute {ι : Type u_1} {κ : Type u_2} {β : Type u_4} {t : DecisionTree ι β} {f : (ι → Bool) → β} (ht : t.Computes f) {s : ι → DecisionTree κ Bool} {g : ι → (κ → Bool) → Bool} (hs : ∀ (i : ι), (s i).Computes (g i)) : (t.substitute s).Computes fun (x : κ → Bool) => f fun (i : ι) => g i x

Composing trees that compute the supplied functions computes their function composition.

theorem Cslib.DecisionTree.weightedCost_substitute {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (t : DecisionTree ι β) (s : ι → DecisionTree κ Bool) (w : κ → ℕ) (x : κ → Bool) : (t.substitute s).weightedCost w x = t.weightedCost (fun (i : ι) => (s i).weightedCost w x) fun (i : ι) => (s i).eval x

Exact cost of substitution: charge each outer query the cost of its subroutine on the current input. Overlapping variables and repeated queries are both permitted.

theorem Cslib.DecisionTree.cost_substitute {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (t : DecisionTree ι β) (s : ι → DecisionTree κ Bool) (x : κ → Bool) : (t.substitute s).cost x = t.weightedCost (fun (i : ι) => (s i).cost x) fun (i : ι) => (s i).eval x

Exact query count after substitution, with the executed inner query counts as weights.

theorem Cslib.DecisionTree.weightedDepth_substitute_le {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (t : DecisionTree ι β) (s : ι → DecisionTree κ Bool) (w : κ → ℕ) : (t.substitute s).weightedDepth w ≤ t.weightedDepth fun (i : ι) => (s i).weightedDepth w

Bound each inner computation by its weighted structural depth and add these bounds along the outer tree. An inner tree's most expensive leaf need not select the most expensive continuation, so this is an inequality.

theorem Cslib.DecisionTree.depth_substitute_le {ι : Type u_1} {κ : Type u_2} {β : Type u_4} (t : DecisionTree ι β) (s : ι → DecisionTree κ Bool) : (t.substitute s).depth ≤ t.weightedDepth fun (i : ι) => (s i).depth

Substitution depth is bounded by charging each outer query the depth of its subroutine.

theorem Cslib.DecisionTree.complexity_substitute_le {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [Finite κ] {t : DecisionTree ι β} {f : (ι → Bool) → β} (ht : t.Computes f) (g : ι → (κ → Bool) → Bool) : (complexity fun (x : κ → Bool) => f fun (i : ι) => g i x) ≤ t.weightedDepth fun (i : ι) => complexity (g i)

Any outer decision tree gives a composition bound weighted by the optimal inner depths. The inner functions may all read the same input variables.

theorem Cslib.DecisionTree.complexity_substitute_le_mul {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [Finite ι] [Finite κ] (f : (ι → Bool) → β) (g : ι → (κ → Bool) → Bool) {d : ℕ} (hg : ∀ (i : ι), complexity (g i) ≤ d) : (complexity fun (x : κ → Bool) => f fun (i : ι) => g i x) ≤ complexity f * d

If each inner function has complexity at most d, composition has complexity at most the outer complexity times d. No disjointness of the inner inputs is required.

theorem Cslib.DecisionTree.complexity_blockCompose_le {ι : Type u_1} {β : Type u_4} {κ : ι → Type u_7} [∀ (i : ι), Finite (κ i)] {t : DecisionTree ι β} {f : (ι → Bool) → β} (ht : t.Computes f) (g : (i : ι) → (κ i → Bool) → Bool) : (complexity fun (x : (i : ι) × κ i → Bool) => f fun (i : ι) => g i fun (j : κ i) => x ⟨i, j⟩) ≤ t.weightedDepth fun (i : ι) => complexity (g i)

A weighted bound for composition on disjoint, possibly differently sized finite blocks.

theorem Cslib.DecisionTree.complexity_blockCompose_le_mul {ι : Type u_1} {β : Type u_4} {κ : ι → Type u_7} [Finite ι] [∀ (i : ι), Finite (κ i)] (f : (ι → Bool) → β) (g : (i : ι) → (κ i → Bool) → Bool) {d : ℕ} (hg : ∀ (i : ι), complexity (g i) ≤ d) : (complexity fun (x : (i : ι) × κ i → Bool) => f fun (i : ι) => g i fun (j : κ i) => x ⟨i, j⟩) ≤ complexity f * d

Uniform-cost composition on disjoint finite blocks; empty blocks and constant functions are included. The construction proves an upper bound only.