Finite unbounded connectives

Public evaluation, size, and depth laws for list conjunctions and disjunctions. Empty lists are included. These laws support compilation of finite quantifiers.

theorem Complexity.AC0Formula.eval_andList {N : ℕ} (input : BitString N) (fs : List (AC0Formula N)) : eval input (andList fs) = fs.all (eval input)

List conjunction evaluates by Boolean all.

theorem Complexity.AC0Formula.eval_orList {N : ℕ} (input : BitString N) (fs : List (AC0Formula N)) : eval input (orList fs) = fs.any (eval input)

List disjunction evaluates by Boolean any.

theorem Complexity.AC0Formula.size_andList {N : ℕ} (fs : List (AC0Formula N)) : (andList fs).size = 1 + (List.map size fs).sum

A conjunction adds one gate to the sum of child sizes.

theorem Complexity.AC0Formula.size_orList {N : ℕ} (fs : List (AC0Formula N)) : (orList fs).size = 1 + (List.map size fs).sum

A disjunction adds one gate to the sum of child sizes.

theorem Complexity.AC0Formula.forestDepth_ofList_le {N : ℕ} (fs : List (AC0Formula N)) (d : ℕ) (h : ∀ f ∈ fs, f.depth ≤ d) : forestDepth (AC0Forest.ofList fs) ≤ d

A uniform bound on child depths bounds their forest depth.

theorem Complexity.AC0Formula.depth_andList_le {N : ℕ} (fs : List (AC0Formula N)) (d : ℕ) (h : ∀ f ∈ fs, f.depth ≤ d) : (andList fs).depth ≤ d + 1

List conjunction adds at most one layer to a common child-depth bound.

theorem Complexity.AC0Formula.depth_orList_le {N : ℕ} (fs : List (AC0Formula N)) (d : ℕ) (h : ∀ f ∈ fs, f.depth ≤ d) : (orList fs).depth ≤ d + 1

List disjunction adds at most one layer to a common child-depth bound.