Iterated switching for AC0 formulas -- definitions

A restriction stage is stored newest first. The tail therefore contains the earlier stages used to simplify the children of a gate, while the head is the next restriction used to switch the normal form assembled at that gate.

This representation is finite and nonuniform. It contains restrictions and formula trees only; it does not contain or assume a circuit generator.

def Complexity.Switching.RestrictionStages (N : ℕ) : ℕ → Type

A newest-first sequence of exactly stageCount finite restrictions.

Equations

• Complexity.Switching.RestrictionStages N 0 = Unit
• Complexity.Switching.RestrictionStages N stageCount.succ = (Complexity.Restriction.On N × Complexity.Switching.RestrictionStages N stageCount)

def Complexity.Switching.RestrictionStages.cumulative {N : ℕ} (stageCount : ℕ) : RestrictionStages N stageCount → Restriction.On N

Compose all stages chronologically, so earlier fixed values take precedence over later stages.

Equations

• Complexity.Switching.RestrictionStages.cumulative 0 x_2 = Complexity.Restriction.On.empty
• Complexity.Switching.RestrictionStages.cumulative stageCount.succ stages = (Complexity.Switching.RestrictionStages.cumulative stageCount stages.2).comp stages.1

def Complexity.RandomRestriction.StageSeed (N q : ℕ) : ℕ → Type

Independent sparse-restriction seeds for exactly stageCount stages. The recursive product stores the earlier stages before the newest seed.

Equations

• Complexity.RandomRestriction.StageSeed N q 0 = Unit
• Complexity.RandomRestriction.StageSeed N q stageCount.succ = (Complexity.RandomRestriction.StageSeed N q stageCount × Complexity.RandomRestriction.Seed N q)

@[implicit_reducible]

instance Complexity.RandomRestriction.stageSeedFintype (N q stageCount : ℕ) : Fintype (StageSeed N q stageCount)

Equations

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

@[implicit_reducible]

instance Complexity.RandomRestriction.stageSeedDecidableEq (N q stageCount : ℕ) : DecidableEq (StageSeed N q stageCount)

Equations

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

def Complexity.RandomRestriction.decodeStages {N q stageCount : ℕ} : StageSeed N q stageCount → Switching.RestrictionStages N stageCount

Decode every seed in a staged sparse restriction.

Equations

• Complexity.RandomRestriction.decodeStages x_2 = ()
• Complexity.RandomRestriction.decodeStages seeds = (Complexity.RandomRestriction.decode seeds.2, Complexity.RandomRestriction.decodeStages seeds.1)

def Complexity.RandomRestriction.finalRestriction {N q stageCount : ℕ} (seeds : StageSeed N q stageCount) : Restriction.On N

The cumulative finite restriction decoded from all stages.

Equations

• Complexity.RandomRestriction.finalRestriction seeds = Complexity.Switching.RestrictionStages.cumulative stageCount (Complexity.RandomRestriction.decodeStages seeds)

def Complexity.RandomRestriction.stageEventCount {N stageCount : ℕ} (q : ℕ) (event : Switching.RestrictionStages N stageCount → Prop) [DecidablePred event] : ℕ

Count staged seeds whose decoded restrictions satisfy event.

Equations

• Complexity.RandomRestriction.stageEventCount q event = {seeds : Complexity.RandomRestriction.StageSeed N q stageCount | event (Complexity.RandomRestriction.decodeStages seeds)}.card

def Complexity.RandomRestriction.stageFreeSum (N q stageCount : ℕ) : ℕ

Sum, over all staged seeds, of the number of variables left free by the cumulative restriction.

Equations

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

def Complexity.AC0Formula.baseDecisionTree {N : ℕ} : AC0Formula N → DecisionTree.On N

The depth-at-most-one decision tree used at the bottom of the staged compiler. Gate cases are a harmless fallback: correctness uses this construction only when the formula has connective depth zero.

Equations

• One or more equations did not get rendered due to their size.
• (Complexity.AC0Formula.const value).baseDecisionTree = Complexity.DecisionTree.On.leaf value
• (Complexity.AC0Formula.and children).baseDecisionTree = Complexity.DecisionTree.On.leaf (Complexity.AC0Formula.evalAll (fun (x : Fin N) => false) children)
• (Complexity.AC0Formula.or children).baseDecisionTree = Complexity.DecisionTree.On.leaf (Complexity.AC0Formula.evalAny (fun (x : Fin N) => false) children)

noncomputable def Complexity.AC0Formula.stagedDecisionTree {N : ℕ} (stageCount : ℕ) : Switching.RestrictionStages N stageCount → AC0Formula N → DecisionTree.On N

Compile a depth-bounded AC0 formula through a newest-first sequence of switching stages.

At a gate, the earlier stages recursively compile every child to a decision tree. A conjunction of those trees becomes a CNF and a disjunction becomes a DNF. The newest restriction is then handled by the corresponding complete block switching tree.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.AC0Formula.stagedDecisionTree 0 x_3 x✝ = x✝.baseDecisionTree

def Complexity.AC0Formula.stagedBad {N stageCount : ℕ} (formula : AC0Formula N) (queryCount : ℕ) (stages : Switching.RestrictionStages N stageCount) : Prop

The staged compiler fails its target depth when its output has depth at least queryCount.

Equations

• formula.stagedBad queryCount stages = (queryCount ≤ (Complexity.AC0Formula.stagedDecisionTree stageCount stages formula).depth)

@[implicit_reducible]

noncomputable instance Complexity.AC0Formula.stagedBadDecidable {N : ℕ} (formula : AC0Formula N) (queryCount stageCount : ℕ) : DecidablePred (formula.stagedBad queryCount)

Equations

• formula.stagedBadDecidable queryCount stageCount stages = id inferInstance