Stack-free streams for finite Boolean folds — definitions

Right-associated finite conjunctions and disjunctions have linear tree depth. Their raw compilation nevertheless has a simple streaming order: compile every member from left to right, emit one terminal constant, then emit the binary connectors from right to left. This module names the connector suffix used by that decomposition.

def Complexity.BoolFormula.rightFoldSize (formulas : List BoolFormula) : ℕ

Tree size shared by a right-associated conjunction or disjunction over formulas.

Equations

• Complexity.BoolFormula.rightFoldSize formulas = 1 + (List.map (fun (formula : Complexity.BoolFormula) => formula.size + 1) formulas).sum

def Complexity.BoolFormula.rightFoldConnectors (op : AndOrOp) (available : ℕ) : List BoolFormula → CircuitCode.RawCircuit

Connector gates completing a right-associated finite Boolean fold.

The recursive call emits the deeper, right-hand connectors first. The final gate combines the current member output with the completed tail output.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BoolFormula.rightFoldConnectors op available [] = []

def Complexity.BoolFormula.compileRawRightFold (op : AndOrOp) (identity : Bool) (available : ℕ) (formulas : List BoolFormula) : CircuitCode.RawCircuit

Explicit stack-free raw stream for a finite Boolean fold. Members are compiled forward, the identity constant is emitted once, and connectors are emitted in reverse member order.

Equations

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