AND/OR/NOT Basis — Definitions

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

Main definitions

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

inductive Complexity.AndOrOp : 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 : AndOrOp

  The AND operation: outputs true iff all inputs are true.

• or : AndOrOp

  The OR operation: outputs true iff at least one input is true.

def Complexity.instReprAndOrOp.repr : AndOrOp → ℕ → Std.Format

Equations

• Complexity.instReprAndOrOp.repr Complexity.AndOrOp.and prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.AndOrOp.and")).group prec✝
• Complexity.instReprAndOrOp.repr Complexity.AndOrOp.or prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.AndOrOp.or")).group prec✝

@[implicit_reducible]

instance Complexity.instReprAndOrOp : Repr AndOrOp

Equations

• Complexity.instReprAndOrOp = { reprPrec := Complexity.instReprAndOrOp.repr }

@[implicit_reducible]

instance Complexity.instDecidableEqAndOrOp : DecidableEq AndOrOp

Equations

• Complexity.instDecidableEqAndOrOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Complexity.AndOrOp.eval (op : AndOrOp) (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

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

def Complexity.Basis.unboundedAndOr : 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 Complexity.Basis.boundedAndOr (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 Complexity.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 Complexity.fanIn_andOr2 {W : ℕ} (g : Gate Basis.andOr2 W) : g.fanIn = 2

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

theorem Complexity.AndOrOp.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 Complexity.AndOrOp.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.