Bases of Boolean operations

This file defines bit strings, families of Boolean functions, and the bases of Boolean operations over which circuits are built.

Each basis is also a CSLib signature, so CSLib's circuits (Cslib.Circuits.Circuit, straight-line programs over a signature) can be built over it without changing its cost model. An operation symbol of B.signature is a whole gate kind of B: an operation, a fan-in that the operation allows, and a negation flag for each input. Its interpretation B.interpretation negates the flagged inputs and applies the operation, so negations stay free, and a basis with unbounded fan-in becomes a signature with infinitely many operation symbols. CSLib's size over B.signature is thus this library's convention (one unit per gate, whatever its fan-in or negation pattern), not the size over CSLib's De Morgan basis, which charges negation gates; Complexitylib.Interop.Cslib.Circuit relates the two.

Main definitions

• BitString — a string of bits of a specific length
• BoolFunFamily — a family of Boolean functions indexed by input length
• Arity — an arity constraint for the operations of a basis
• Basis — a basis of Boolean operations with arity constraints
• Basis.GateKind, Basis.signature, Basis.interpretation — a basis as a CSLib signature and its Boolean interpretation

@[reducible, inline]

abbrev Complexity.BitString (n : ℕ) : Type

A BitString of length n.

Equations

• Complexity.BitString n = (Fin n → Bool)

@[reducible, inline]

abbrev Complexity.BoolFunFamily : Type

A family of Boolean functions indexed by input length N.

Each member maps N-bit strings to a single output bit.

Equations

• Complexity.BoolFunFamily = ((N : ℕ) → Complexity.BitString N → Bool)

inductive Complexity.Arity : Type

Arity constraint for operations in a basis.

• unbounded : Arity

  Any number of inputs is allowed.

• exactly (k : ℕ) : Arity

  Exactly k inputs are required.

• upto (k : ℕ) : Arity

  At most k inputs are allowed.

@[instance_reducible]

instance Complexity.instReprArity : Repr Arity

Equations

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

def Complexity.instReprArity.repr : Arity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Complexity.instReprArity.repr Complexity.Arity.unbounded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Complexity.Arity.unbounded")).group prec✝

@[instance_reducible]

instance Complexity.instDecidableEqArity : DecidableEq Arity

Equations

• Complexity.instDecidableEqArity = Complexity.instDecidableEqArity.decEq

def Complexity.instDecidableEqArity.decEq (x✝ x✝¹ : Arity) : Decidable (x✝ = x✝¹)

Equations

• Complexity.instDecidableEqArity.decEq Complexity.Arity.unbounded Complexity.Arity.unbounded = isTrue ⋯
• Complexity.instDecidableEqArity.decEq Complexity.Arity.unbounded (Complexity.Arity.exactly k) = isFalse ⋯
• Complexity.instDecidableEqArity.decEq Complexity.Arity.unbounded (Complexity.Arity.upto k) = isFalse ⋯
• Complexity.instDecidableEqArity.decEq (Complexity.Arity.exactly k) Complexity.Arity.unbounded = isFalse ⋯
• Complexity.instDecidableEqArity.decEq (Complexity.Arity.exactly a) (Complexity.Arity.exactly b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.instDecidableEqArity.decEq (Complexity.Arity.exactly k) (Complexity.Arity.upto k_1) = isFalse ⋯
• Complexity.instDecidableEqArity.decEq (Complexity.Arity.upto k) Complexity.Arity.unbounded = isFalse ⋯
• Complexity.instDecidableEqArity.decEq (Complexity.Arity.upto k) (Complexity.Arity.exactly k_1) = isFalse ⋯
• Complexity.instDecidableEqArity.decEq (Complexity.Arity.upto a) (Complexity.Arity.upto b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Complexity.Arity.satisfiedBy : Arity → ℕ → Prop

Whether n satisfies an arity constraint.

Equations

• Complexity.Arity.unbounded.satisfiedBy x✝ = True
• (Complexity.Arity.exactly k).satisfiedBy x✝ = (x✝ = k)
• (Complexity.Arity.upto k).satisfiedBy x✝ = (x✝ ≤ k)

@[instance_reducible]

instance Complexity.instDecidableSatisfiedBy (a : Arity) (n : ℕ) : Decidable (a.satisfiedBy n)

Equations

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

structure Complexity.Basis : Type 1

A basis of Boolean operations.

Each operation has an arity constraint and an evaluation function that computes the output bit from any valid number of input bits.

• Op : Type

  The type of operations (e.g., AND, OR, NOT).

• arity : self.Op → Arity

  The arity constraint for each operation.

• eval (op : self.Op) (n : ℕ) : (self.arity op).satisfiedBy n → BitString n → Bool

  Evaluate an operation on n input bits, given that n satisfies the arity.

structure Complexity.Basis.GateKind (B : Basis) : Type

A gate kind of the basis B: an operation, a fan-in that the operation allows, and a negation flag for each input.

• op : B.Op

  The basis operation.

• fanIn : ℕ

  The number of inputs.

• arityOk : (B.arity self.op).satisfiedBy self.fanIn

  The operation allows this fan-in.

• negated : Fin self.fanIn → Bool

  Which inputs are negated before the operation is applied.

def Complexity.Basis.signature (B : Basis) : Cslib.Circuits.Signature

The CSLib signature of a basis: one operation symbol per gate kind, with the gate kind's fan-in as its arity.

Equations

• B.signature = { Op := B.GateKind, Arity := fun (kind : B.GateKind) => kind.fanIn }

def Complexity.Basis.interpretation (B : Basis) : Cslib.Circuits.Interpretation B.signature Bool

The interpretation of a basis's signature: a gate kind negates the flagged inputs and applies its operation, exactly as Gate.eval does (Basis.interpretation_kind in Complexitylib.Circuits.StraightLine).

Equations

• B.interpretation kind input = B.eval kind.op kind.fanIn ⋯ fun (i : Fin kind.fanIn) => kind.negated i ^^ input i