The canonical decision tree of a restricted formula

Let F be a formula in disjunctive normal form and ρ a restriction (partial assignment). The canonical decision tree of F under ρ finds the first term of F that ρ does not falsify (DNF.firstTerm), queries its free variables (DNF.queried), and continues under ρ extended by the answers; when nothing is left to query, F is constant under ρ and the tree outputs its value (DNF.canonicalTree, DNF.eval_canonicalTree). Its depth is at most the largest number of variables it queries on an input (DNF.depth_canonicalTree_le, DNF.pathLength), which is what the switching lemma bounds [Has86], [Raz95], Jukna, Chapter 12.

Main definitions

• Cslib.Logic.PL.DNF.firstTerm, Cslib.Logic.PL.DNF.queried.
• Cslib.Logic.PL.DNF.canonicalTree, Cslib.Logic.PL.DNF.pathLength.

Main results

• Cslib.Logic.PL.DNF.eval_canonicalTree: the canonical tree computes the restricted formula.
• Cslib.Logic.PL.DNF.complexity_lt_of_forall_pathLength_lt: short query paths give shallow decision trees.

References

• J. Håstad, Almost optimal lower bounds for small depth circuits
• A. A. Razborov, Bounded arithmetic and lower bounds in Boolean complexity
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Logic.PL.Term.FalsifiedBy {ι : Type u_1} (t : Term ι) (ρ : BitString.PartialAssignment ι) : Prop

The restriction ρ falsifies the term t: it fixes one of its variables to the other value.

@[instance_reducible]

instance Cslib.Logic.PL.Term.instDecidableFalsifiedBy {ι : Type u_1} (t : Term ι) (ρ : BitString.PartialAssignment ι) : Decidable (t.FalsifiedBy ρ)

def Cslib.Logic.PL.Term.freeVars {ι : Type u_1} (t : Term ι) (ρ : BitString.PartialAssignment ι) : List ι

The variables of the term t left free by ρ, in order.

theorem Cslib.Logic.PL.Term.mem_freeVars {ι : Type u_1} {t : Term ι} {ρ : BitString.PartialAssignment ι} {v : ι} : v ∈ t.freeVars ρ ↔ ∃ (b : Bool), (v, b) ∈ t ∧ ρ v = none

def Cslib.Logic.PL.DNF.firstTerm {ι : Type u_1} (F : DNF ι) (ρ : BitString.PartialAssignment ι) : Option (Term ι)

The first term of F not falsified by ρ.

def Cslib.Logic.PL.DNF.queried {ι : Type u_1} (F : DNF ι) (ρ : BitString.PartialAssignment ι) : List ι

The variables queried at ρ: the free variables of the first term not falsified by ρ.

theorem Cslib.Logic.PL.DNF.free_of_mem_queried {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} {v : ι} (hv : v ∈ F.queried ρ) : ρ v = none

theorem Cslib.Logic.PL.DNF.toFinset_queried_subset_free {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] : (F.queried ρ).toFinset ⊆ ρ.free

theorem Cslib.Logic.PL.DNF.card_free_assign_lt {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] (h : F.queried ρ ≠ []) (a : ι → Bool) : (ρ.assign (F.queried ρ).toFinset a).free.card < ρ.free.card

Answering the queried variables frees fewer variables, as long as something is queried.

@[irreducible]

def Cslib.Logic.PL.DNF.canonicalTree {ι : Type u_1} (F : DNF ι) [Fintype ι] [DecidableEq ι] (ρ : BitString.PartialAssignment ι) : DecisionTree ι Bool

The canonical decision tree of F under ρ: query the free variables of the first term not falsified by ρ, and continue under ρ extended by the answers.

@[irreducible]

def Cslib.Logic.PL.DNF.pathLength {ι : Type u_1} (F : DNF ι) [Fintype ι] [DecidableEq ι] (ρ : BitString.PartialAssignment ι) (x : ι → Bool) : ℕ

The number of variables the canonical tree queries on the input x.

theorem Cslib.Logic.PL.DNF.pathLength_of_queried_eq_nil {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] (h : F.queried ρ = []) (x : ι → Bool) : F.pathLength ρ x = 0

theorem Cslib.Logic.PL.DNF.pathLength_of_queried_ne_nil {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] (h : F.queried ρ ≠ []) (x : ι → Bool) : F.pathLength ρ x = (F.queried ρ).length + F.pathLength (ρ.assign (F.queried ρ).toFinset x) x

theorem Cslib.Logic.PL.DNF.eval_canonicalTree {ι : Type u_1} {F : DNF ι} [Fintype ι] [DecidableEq ι] (ρ : BitString.PartialAssignment ι) (x : ι → Bool) : (F.canonicalTree ρ).eval x = eval (ρ.fill x) F

The canonical tree computes the formula restricted by ρ.

theorem Cslib.Logic.PL.DNF.pathLength_congr {ι : Type u_1} {F : DNF ι} [Fintype ι] [DecidableEq ι] {ρ : BitString.PartialAssignment ι} {x y : ι → Bool} (h : ∀ i ∈ ρ.free, x i = y i) : F.pathLength ρ x = F.pathLength ρ y

The query path depends only on the free bits of the input.

theorem Cslib.Logic.PL.DNF.depth_canonicalTree_le {ι : Type u_1} {F : DNF ι} [Fintype ι] [DecidableEq ι] (ρ : BitString.PartialAssignment ι) : (F.canonicalTree ρ).depth ≤ Finset.univ.sup (F.pathLength ρ)

The canonical tree is no deeper than its longest query path.

theorem Cslib.Logic.PL.DNF.complexity_lt_of_forall_pathLength_lt {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] {s : ℕ} (h : ∀ (x : ι → Bool), F.pathLength ρ x < s) : (DecisionTree.complexity fun (x : ι → Bool) => eval (ρ.fill x) F) < s

If every query path is shorter than s, the restricted formula has decision tree depth less than s.