Semantics-preserving maps between circuit bases -- definitions

A Basis.Hom B₁ B₂ maps every operation-and-arity pair of B₁ to a B₂ operation that accepts that arity and has exactly the same Boolean semantics. The target label may depend on arity: for example, an unbounded AND of fan-in n maps to the threshold operation "at least n." The map changes only gate labels; fan-in, wiring, negation flags, gate count, and circuit topology are preserved exactly.

structure Complexity.Basis.Hom (source target : Basis) : Type

A semantics-preserving operation map between Boolean bases.

• mapOp : source.Op → ℕ → target.Op

  Translate a source operation at a specified gate arity.

• mapArity (op : source.Op) (n : ℕ) : (source.arity op).satisfiedBy n → (target.arity (self.mapOp op n)).satisfiedBy n

  Every legal source arity is legal for the translated operation.

• eval_map (op : source.Op) (n : ℕ) (arityOk : (source.arity op).satisfiedBy n) (inputs : BitString n) : target.eval (self.mapOp op n) n ⋯ inputs = source.eval op n arityOk inputs

  Operation translation preserves semantics exactly.

def Complexity.Gate.mapBasis {source target : Basis} {W : ℕ} (hom : source.Hom target) (gate : Gate source W) : Gate target W

Relabel a gate along a basis homomorphism without changing its topology.

Equations

• Complexity.Gate.mapBasis hom gate = { op := hom.mapOp gate.op gate.fanIn, fanIn := gate.fanIn, arityOk := ⋯, inputs := gate.inputs, negated := gate.negated }

def Complexity.Circuit.mapBasis {N M : ℕ} {source target : Basis} {G : ℕ} [NeZero N] [NeZero M] (hom : source.Hom target) (circuit : Circuit source N M G) : Circuit target N M G

Relabel every gate of a circuit along a basis homomorphism.

Equations

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

def Complexity.CircuitFamily.mapBasis {source target : Basis} (hom : source.Hom target) (family : CircuitFamily source) : CircuitFamily target

Relabel every positive-length circuit in a nonuniform family.

Equations

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