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

theorem Cslib.Logic.PL.Term.eval_fill_of_falsifiedBy {ι : Type u_1} {t : Term ι} {ρ : BitString.PartialAssignment ι} (h : t.FalsifiedBy ρ) (x : ι → Bool) : eval (ρ.fill x) t = false

A falsified term is false on every input filled from the restriction.

theorem Cslib.Logic.PL.Term.eval_fill_of_freeVars_eq_nil {ι : Type u_1} {t : Term ι} {ρ : BitString.PartialAssignment ι} (h : ¬t.FalsifiedBy ρ) (hV : t.freeVars ρ = []) (x : ι → Bool) : eval (ρ.fill x) t = true

A term that is not falsified and has no free variable is true on every input filled from the restriction.

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.eval_fill_of_queried_eq_nil {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} (h : F.queried ρ = []) (x : ι → Bool) : eval (ρ.fill x) F = (F.firstTerm ρ).isSome

When nothing is queried, the formula is constant under the restriction: true exactly when some term is not falsified.

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.canonicalTree_of_queried_eq_nil {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] (h : F.queried ρ = []) : F.canonicalTree ρ = DecisionTree.leaf (eval (ρ.fill fun (x : ι) => false) F)

theorem Cslib.Logic.PL.DNF.canonicalTree_of_queried_ne_nil {ι : Type u_1} {F : DNF ι} {ρ : BitString.PartialAssignment ι} [Fintype ι] [DecidableEq ι] (h : F.queried ρ ≠ []) : F.canonicalTree ρ = DecisionTree.graft (F.queried ρ) (fun (a : ι → Bool) => F.canonicalTree (ρ.assign (F.queried ρ).toFinset a)) fun (x : ι) => false

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.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.