Boolean decision trees

Decision trees query named input coordinates and branch on their Boolean values. The false branch is stored first. Depth is the largest number of query nodes on a root-to-leaf path.

The semantic restriction operation removes queries fixed by a partial assignment and retains live queries. Its correctness and depth monotonicity are proved structurally. Decision-tree depth bounds are existential propositions; this module does not compute or search for optimal trees.

inductive Algebraic.AC0.DecisionTree (n : ℕ) : Type

A Boolean decision tree on n named input variables.

• leaf {n : ℕ} (value : Bool) : DecisionTree n
• query {n : ℕ} (index : Fin n) (onFalse onTrue : DecisionTree n) : DecisionTree n

def Algebraic.AC0.instDecidableEqDecisionTree.decEq {n✝ : ℕ} (x✝ x✝¹ : DecisionTree n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.instDecidableEqDecisionTree.decEq (Algebraic.AC0.DecisionTree.leaf a) (Algebraic.AC0.DecisionTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Algebraic.AC0.instDecidableEqDecisionTree.decEq (Algebraic.AC0.DecisionTree.leaf value) (Algebraic.AC0.DecisionTree.query index onFalse onTrue) = isFalse ⋯
• Algebraic.AC0.instDecidableEqDecisionTree.decEq (Algebraic.AC0.DecisionTree.query index onFalse onTrue) (Algebraic.AC0.DecisionTree.leaf value) = isFalse ⋯

@[instance_reducible]

instance Algebraic.AC0.instDecidableEqDecisionTree {n✝ : ℕ} : DecidableEq (DecisionTree n✝)

Equations

• Algebraic.AC0.instDecidableEqDecisionTree = Algebraic.AC0.instDecidableEqDecisionTree.decEq

structure Algebraic.AC0.DecisionTree.PathStep (n : ℕ) : Type

One query and branch choice along a decision-tree path.

• index : Fin n

  Coordinate queried at this step.

• value : Bool

  Branch selected at this step.

@[instance_reducible]

instance Algebraic.AC0.DecisionTree.instDecidableEqPathStep {n✝ : ℕ} : DecidableEq (PathStep n✝)

Equations

• Algebraic.AC0.DecisionTree.instDecidableEqPathStep = Algebraic.AC0.DecisionTree.instDecidableEqPathStep.decEq

def Algebraic.AC0.DecisionTree.instDecidableEqPathStep.decEq {n✝ : ℕ} (x✝ x✝¹ : PathStep n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

inductive Algebraic.AC0.DecisionTree.Path {n : ℕ} : DecisionTree n → List (PathStep n) → DecisionTree n → Prop

A finite root-to-subtree path. The endpoint need not be a leaf, which lets us take an exact-length prefix of any sufficiently deep branch.

• nil {n : ℕ} (tree : DecisionTree n) : tree.Path [] tree
• takeFalse {n : ℕ} {index : Fin n} {onFalse onTrue endpoint : DecisionTree n} {steps : List (PathStep n)} (tail : onFalse.Path steps endpoint) : (query index onFalse onTrue).Path ({ index := index, value := false } :: steps) endpoint
• takeTrue {n : ℕ} {index : Fin n} {onFalse onTrue endpoint : DecisionTree n} {steps : List (PathStep n)} (tail : onTrue.Path steps endpoint) : (query index onFalse onTrue).Path ({ index := index, value := true } :: steps) endpoint

def Algebraic.AC0.DecisionTree.eval {n : ℕ} : DecisionTree n → (Fin n → Bool) → Bool

Evaluate a decision tree on a complete input.

Equations

• (Algebraic.AC0.DecisionTree.leaf value).eval x✝ = value
• (Algebraic.AC0.DecisionTree.query index onFalse onTrue).eval x✝ = if x✝ index = true then onTrue.eval x✝ else onFalse.eval x✝

@[simp]

theorem Algebraic.AC0.DecisionTree.eval_leaf {n : ℕ} (value : Bool) (input : Fin n → Bool) : (leaf value).eval input = value

@[simp]

theorem Algebraic.AC0.DecisionTree.eval_query {n : ℕ} (index : Fin n) (onFalse onTrue : DecisionTree n) (input : Fin n → Bool) : (query index onFalse onTrue).eval input = if input index = true then onTrue.eval input else onFalse.eval input

def Algebraic.AC0.DecisionTree.depth {n : ℕ} : DecisionTree n → ℕ

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

Equations

• (Algebraic.AC0.DecisionTree.leaf value).depth = 0
• (Algebraic.AC0.DecisionTree.query index onFalse onTrue).depth = (max onFalse.depth onTrue.depth).succ

@[simp]

theorem Algebraic.AC0.DecisionTree.depth_leaf {n : ℕ} (value : Bool) : (leaf value).depth = 0

@[simp]

theorem Algebraic.AC0.DecisionTree.depth_query {n : ℕ} (index : Fin n) (onFalse onTrue : DecisionTree n) : (query index onFalse onTrue).depth = (max onFalse.depth onTrue.depth).succ

theorem Algebraic.AC0.DecisionTree.Path.length_add_endpoint_depth_le {n : ℕ} {tree endpoint : DecisionTree n} {steps : List (PathStep n)} (path : tree.Path steps endpoint) : steps.length + endpoint.depth ≤ tree.depth

Traversing a path consumes at most the depth of its source tree. The strong form retains the depth still available at the endpoint.

theorem Algebraic.AC0.DecisionTree.exists_path_of_length_le_depth {n : ℕ} (tree : DecisionTree n) (length : ℕ) (available : length ≤ tree.depth) : ∃ (steps : List (PathStep n)) (endpoint : DecisionTree n), tree.Path steps endpoint ∧ steps.length = length

Every requested length not exceeding the tree depth occurs as the length of a root-to-subtree path.

def Algebraic.AC0.DecisionTree.PathStep.indices {n : ℕ} (steps : List (PathStep n)) : List (Fin n)

The queried coordinates of a path transcript.

Equations

• Algebraic.AC0.DecisionTree.PathStep.indices steps = List.map Algebraic.AC0.DecisionTree.PathStep.index steps

def Algebraic.AC0.DecisionTree.PathStep.assignment {n : ℕ} : List (PathStep n) → PartialAssignment n

The partial assignment made by a path transcript. Earlier occurrences win; canonical paths will later be proved duplicate-free.

Equations

• Algebraic.AC0.DecisionTree.PathStep.assignment [] = Algebraic.PartialAssignment.empty
• Algebraic.AC0.DecisionTree.PathStep.assignment (step :: rest) = (Algebraic.PartialAssignment.fix step.index step.value).refine (Algebraic.AC0.DecisionTree.PathStep.assignment rest)

def Algebraic.AC0.DecisionTree.ReadOnceWithin {n : ℕ} : DecisionTree n → Finset (Fin n) → Prop

Every root-to-leaf path queries distinct coordinates drawn from the given available set. At a query node, that coordinate is removed before checking either child.

Equations

• (Algebraic.AC0.DecisionTree.leaf value).ReadOnceWithin x✝ = True
• (Algebraic.AC0.DecisionTree.query index onFalse onTrue).ReadOnceWithin x✝ = (index ∈ x✝ ∧ onFalse.ReadOnceWithin (x✝.erase index) ∧ onTrue.ReadOnceWithin (x✝.erase index))

@[simp]

theorem Algebraic.AC0.DecisionTree.PathStep.assignment_nil {n : ℕ} : assignment [] = PartialAssignment.empty

@[simp]

theorem Algebraic.AC0.DecisionTree.PathStep.assignment_cons {n : ℕ} (step : PathStep n) (rest : List (PathStep n)) : assignment (step :: rest) = (PartialAssignment.fix step.index step.value).refine (assignment rest)

theorem Algebraic.AC0.DecisionTree.PathStep.fixedVariables_assignment {n : ℕ} (steps : List (PathStep n)) : (assignment steps).fixedVariables = (indices steps).toFinset

A transcript assignment fixes exactly the coordinates appearing in its query list.

theorem Algebraic.AC0.DecisionTree.PathStep.fixedCount_assignment_eq_length {n : ℕ} (steps : List (PathStep n)) (nodup : (indices steps).Nodup) : (assignment steps).fixedCount = steps.length

A duplicate-free transcript of length s fixes exactly s variables.

theorem Algebraic.AC0.DecisionTree.Path.indices_nodup_and_subset_of_readOnceWithin {n : ℕ} {tree endpoint : DecisionTree n} {steps : List (PathStep n)} {available : Finset (Fin n)} (path : tree.Path steps endpoint) (readOnce : tree.ReadOnceWithin available) : (PathStep.indices steps).Nodup ∧ (PathStep.indices steps).toFinset ⊆ available

A path through a read-once tree has no repeated coordinate, and all its coordinates lie in the original available set.

def Algebraic.AC0.DecisionTree.leafCount {n : ℕ} : DecisionTree n → ℕ

Number of leaves in a decision tree.

Equations

• (Algebraic.AC0.DecisionTree.leaf value).leafCount = 1
• (Algebraic.AC0.DecisionTree.query index onFalse onTrue).leafCount = onFalse.leafCount + onTrue.leafCount

@[simp]

theorem Algebraic.AC0.DecisionTree.leafCount_leaf {n : ℕ} (value : Bool) : (leaf value).leafCount = 1

@[simp]

theorem Algebraic.AC0.DecisionTree.leafCount_query {n : ℕ} (index : Fin n) (onFalse onTrue : DecisionTree n) : (query index onFalse onTrue).leafCount = onFalse.leafCount + onTrue.leafCount

def Algebraic.AC0.DecisionTree.Computes {n : ℕ} (tree : DecisionTree n) (function : ScalarFunction Bool n) : Prop

A tree computes a scalar Boolean function pointwise.

Equations

• tree.Computes function = ∀ (input : Fin n → Bool), tree.eval input = function input

def Algebraic.AC0.DecisionTree.negate {n : ℕ} : DecisionTree n → DecisionTree n

Negate every leaf of a decision tree.

Equations

• (Algebraic.AC0.DecisionTree.leaf value).negate = Algebraic.AC0.DecisionTree.leaf !value
• (Algebraic.AC0.DecisionTree.query index onFalse onTrue).negate = Algebraic.AC0.DecisionTree.query index onFalse.negate onTrue.negate

@[simp]

theorem Algebraic.AC0.DecisionTree.eval_negate {n : ℕ} (tree : DecisionTree n) (input : Fin n → Bool) : tree.negate.eval input = !tree.eval input

@[simp]

theorem Algebraic.AC0.DecisionTree.depth_negate {n : ℕ} (tree : DecisionTree n) : tree.negate.depth = tree.depth

theorem Algebraic.AC0.DecisionTree.Computes.negate {n : ℕ} {tree : DecisionTree n} {function : ScalarFunction Bool n} (computes : tree.Computes function) : tree.negate.Computes fun (input : Fin n → Bool) => !function input

Negating a computing tree computes the pointwise complement.

def Algebraic.AC0.DecisionTree.restrict {n : ℕ} (rho : PartialAssignment n) : DecisionTree n → DecisionTree n

Restrict a decision tree, selecting a branch at fixed queries and retaining queries of live variables. Repeated queries are all simplified.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.DecisionTree.restrict rho (Algebraic.AC0.DecisionTree.leaf value) = Algebraic.AC0.DecisionTree.leaf value

@[simp]

theorem Algebraic.AC0.DecisionTree.eval_restrict {n : ℕ} (tree : DecisionTree n) (rho : PartialAssignment n) (input : Fin n → Bool) : (restrict rho tree).eval input = tree.eval (rho.apply input)

Tree restriction agrees exactly with semantic input restriction.

theorem Algebraic.AC0.DecisionTree.depth_restrict_le {n : ℕ} (tree : DecisionTree n) (rho : PartialAssignment n) : (restrict rho tree).depth ≤ tree.depth

Restriction cannot increase decision-tree depth.

theorem Algebraic.AC0.DecisionTree.restrict_refine {n : ℕ} (tree : DecisionTree n) (rho sigma : PartialAssignment n) : restrict sigma (restrict rho tree) = restrict (rho.refine sigma) tree

Sequential semantic restrictions compose structurally on decision trees.

theorem Algebraic.AC0.DecisionTree.Computes.restrict {n : ℕ} {tree : DecisionTree n} {function : ScalarFunction Bool n} (computes : tree.Computes function) (rho : PartialAssignment n) : (DecisionTree.restrict rho tree).Computes (function.restrict rho)

Restricting a computing tree computes the restricted scalar function.

def Algebraic.AC0.DecisionTree.build {n : ℕ} (indices : List (Fin n)) : ScalarFunction Bool n → DecisionTree n

Build the full Shannon decision tree over an ordered list of coordinates. At the empty list the remaining function is evaluated on the all-false input; the correctness theorem below states the dependency condition under which that choice is immaterial.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.DecisionTree.build [] x✝ = Algebraic.AC0.DecisionTree.leaf (x✝ fun (x : Fin n) => false)

theorem Algebraic.AC0.DecisionTree.depth_build_le_length {n : ℕ} (indices : List (Fin n)) (function : ScalarFunction Bool n) : (build indices function).depth ≤ indices.length

The Shannon tree over a list of coordinates has depth at most the length of that list.

theorem Algebraic.AC0.DecisionTree.build_computes_of_dependsOnlyOn {n : ℕ} (indices : List (Fin n)) (function : ScalarFunction Bool n) (nodup : indices.Nodup) (depends : DependsOnlyOn function indices.toFinset) : (build indices function).Computes function

The Shannon tree computes any function that depends only on its duplicate- free query list.

def Algebraic.AC0.DecisionTree.DepthAtMost {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : Prop

A function has decision-tree depth at most bound when some computing tree has depth at most that bound. No minimization procedure is part of this definition.

Equations

• Algebraic.AC0.DecisionTree.DepthAtMost function bound = ∃ (tree : Algebraic.AC0.DecisionTree n), tree.Computes function ∧ tree.depth ≤ bound

def Algebraic.AC0.DecisionTree.DepthAtLeast {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : Prop

Every decision tree computing the function has depth at least bound.

Equations

• Algebraic.AC0.DecisionTree.DepthAtLeast function bound = ∀ (tree : Algebraic.AC0.DecisionTree n), tree.Computes function → bound ≤ tree.depth

@[instance_reducible]

noncomputable instance Algebraic.AC0.DecisionTree.depthAtMostDecidable {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : Decidable (DepthAtMost function bound)

Proof-level decidability of the semantic upper-depth predicate. This is a classical instance for forming exact finite events; it does not define or run an optimal decision-tree search.

Equations

• Algebraic.AC0.DecisionTree.depthAtMostDecidable function bound = Classical.propDecidable (Algebraic.AC0.DecisionTree.DepthAtMost function bound)

@[instance_reducible]

noncomputable instance Algebraic.AC0.DecisionTree.depthAtLeastDecidable {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : Decidable (DepthAtLeast function bound)

Proof-level decidability of the semantic lower-depth predicate. This is a classical instance for forming exact finite events; it does not define or run an optimal decision-tree search.

Equations

• Algebraic.AC0.DecisionTree.depthAtLeastDecidable function bound = Classical.propDecidable (Algebraic.AC0.DecisionTree.DepthAtLeast function bound)

theorem Algebraic.AC0.DecisionTree.depthAtMost_inputCount {n : ℕ} (function : ScalarFunction Bool n) : DepthAtMost function n

Every n-variable Boolean function has a decision tree of depth at most n. This is a structural Shannon expansion, not an optimal-tree search.

theorem Algebraic.AC0.DecisionTree.DepthAtMost.mono {n : ℕ} {function : ScalarFunction Bool n} {smaller larger : ℕ} (bounded : DepthAtMost function smaller) (le : smaller ≤ larger) : DepthAtMost function larger

A larger allowance preserves an upper decision-tree depth bound.

theorem Algebraic.AC0.DecisionTree.DepthAtMost.restrict {n : ℕ} {function : ScalarFunction Bool n} {bound : ℕ} (bounded : DepthAtMost function bound) (rho : PartialAssignment n) : DepthAtMost (function.restrict rho) bound

Restriction preserves any upper bound on decision-tree depth.

theorem Algebraic.AC0.DecisionTree.depthAtLeast_succ_iff_not_depthAtMost {n : ℕ} (function : ScalarFunction Bool n) (bound : ℕ) : DepthAtLeast function (bound + 1) ↔ ¬DepthAtMost function bound

Depth at least bound + 1 is exactly failure to have depth at most bound.

theorem Algebraic.AC0.DecisionTree.depthAtMost_zero_iff_constant {n : ℕ} (function : ScalarFunction Bool n) : DepthAtMost function 0 ↔ ∃ (value : Bool), ∀ (input : Fin n → Bool), function input = value

A function has depth zero exactly when it is constant.