Postfix Boolean-formula streams

Boolean formulas compile to a flat postfix token stream. A small stack machine reconstructs the tree without a recursive bit-level parser, and the stream has exactly one token for every formula node.

def ComplexityTheory.BooleanFormulaCode.tokens : BooleanFormula → List Token

Compile a formula tree to its canonical postfix token stream. Children precede their connective, so a left-to-right stack machine can rebuild the tree.

Equations

• One or more equations did not get rendered due to their size.
• ComplexityTheory.BooleanFormulaCode.tokens (ComplexityTheory.BooleanFormula.var index) = [ComplexityTheory.BooleanFormulaCode.Token.var index]
• ComplexityTheory.BooleanFormulaCode.tokens ComplexityTheory.BooleanFormula.tru = [ComplexityTheory.BooleanFormulaCode.Token.tru]
• ComplexityTheory.BooleanFormulaCode.tokens ComplexityTheory.BooleanFormula.fls = [ComplexityTheory.BooleanFormulaCode.Token.fls]
• ComplexityTheory.BooleanFormulaCode.tokens formula.neg = ComplexityTheory.BooleanFormulaCode.tokens formula ++ [ComplexityTheory.BooleanFormulaCode.Token.neg]

def ComplexityTheory.BooleanFormulaCode.run? : List Token → List BooleanFormula → Option (List BooleanFormula)

Execute a postfix token stream from an initial formula stack. Evaluation stops with none as soon as a token cannot consume the required operands.

Equations

• ComplexityTheory.BooleanFormulaCode.run? [] x✝ = some x✝
• ComplexityTheory.BooleanFormulaCode.run? (token :: stream) x✝ = do let next ← token.apply? x✝ ComplexityTheory.BooleanFormulaCode.run? stream next

def ComplexityTheory.BooleanFormulaCode.build? (stream : List Token) : Option BooleanFormula

Reconstruct exactly one formula from a complete token stream. Empty streams, stack underflow, and leftover formulas are all rejected.

Equations

• ComplexityTheory.BooleanFormulaCode.build? stream = do let stack ← ComplexityTheory.BooleanFormulaCode.run? stream [] match stack with | [formula] => some formula | x => none

theorem ComplexityTheory.BooleanFormulaCode.run?_append (first second : List Token) (stack : List BooleanFormula) : run? (first ++ second) stack = (run? first stack).bind (run? second)

Running concatenated streams is sequential stack execution. This composition law lets structural proofs reason about each formula subtree independently.

@[simp]

theorem ComplexityTheory.BooleanFormulaCode.run?_tokens (formula : BooleanFormula) (stack : List BooleanFormula) : run? (tokens formula) stack = some (formula :: stack)

Executing a formula's postfix tokens pushes exactly that formula onto any existing stack. This is the central semantic invariant of the stream format.

@[simp]

theorem ComplexityTheory.BooleanFormulaCode.build?_tokens (formula : BooleanFormula) : build? (tokens formula) = some formula

Building from a formula's canonical token stream recovers that formula.

@[simp]

theorem ComplexityTheory.BooleanFormulaCode.length_tokens (formula : BooleanFormula) : (tokens formula).length = formula.size

The postfix stream contains exactly one token per formula-tree node. Token count and syntactic formula size therefore coincide.