AND/OR/NOT Basis — Definitions

This module defines the AND/OR operations and various basis configurations used throughout the circuit complexity library.

Main definitions

• AONOp — AND/OR operations (negation is free via per-input gate flags)
• AONOp.eval — fold-based evaluation of AND/OR on n input bits
• Basis.unboundedAON — unbounded fan-in AND/OR basis
• Basis.boundedAON — fan-in bounded by k AND/OR basis
• Basis.andOr2 — fan-in exactly 2 AND/OR basis (used in Shannon/Schnorr bounds)

inductive CircuitComplexity.AONOp : Type

Operations in an AND/OR basis. Negation is handled by per-input flags on gates, so only AND and OR need explicit representation.

• and : AONOp
• or : AONOp

def CircuitComplexity.instReprAONOp.repr : AONOp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CircuitComplexity.instReprAONOp : Repr AONOp

Equations

• CircuitComplexity.instReprAONOp = { reprPrec := CircuitComplexity.instReprAONOp.repr }

@[implicit_reducible]

instance CircuitComplexity.instDecidableEqAONOp : DecidableEq AONOp

Equations

• CircuitComplexity.instDecidableEqAONOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CircuitComplexity.AONOp.eval (op : AONOp) (n : ℕ) : BitString n → Bool

Evaluate an AND or OR operation on n input bits by folding. AND folds with && starting from true; OR folds with || from false.

Equations

• CircuitComplexity.AONOp.and.eval x✝¹ x✝ = Fin.foldl x✝¹ (fun (acc : Bool) (i : Fin x✝¹) => acc && x✝ i) true
• CircuitComplexity.AONOp.or.eval x✝¹ x✝ = Fin.foldl x✝¹ (fun (acc : Bool) (i : Fin x✝¹) => acc || x✝ i) false

def CircuitComplexity.Basis.unboundedAON : Basis

AND/OR basis with unbounded fan-in. Negation is free (per-input flags on gates).

Equations

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

def CircuitComplexity.Basis.boundedAON (k : ℕ) : Basis

AND/OR basis with fan-in bounded by k. Negation is free (per-input flags on gates).

Equations

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

def CircuitComplexity.Basis.andOr2 : Basis

Fan-in-2 AND/OR basis. Every gate has exactly 2 inputs. Negation is free (per-input flags on gates). This is the basis used in the Shannon and Schnorr lower bound theorems.

Equations

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

theorem CircuitComplexity.andOr2_fanIn {W : ℕ} (g : Gate Basis.andOr2 W) : g.fanIn = 2

Every gate over Basis.andOr2 has fan-in exactly 2.

theorem CircuitComplexity.AONOp.eval_two_and (inputs : BitString 2) : and.eval 2 inputs = (inputs 0 && inputs 1)

A fan-in-2 AND gate computes the conjunction of its two inputs.

theorem CircuitComplexity.AONOp.eval_two_or (inputs : BitString 2) : or.eval 2 inputs = (inputs 0 || inputs 1)

A fan-in-2 OR gate computes the disjunction of its two inputs.