The AND/OR/MOD_m basis -- definitions

This module defines the unbounded-fan-in basis of AND, OR, and MOD_m gates over which the classes AC^i[m] are built. A MOD_m gate outputs true exactly when the number of its true inputs is not divisible by m. Because negation is a free per-input flag, the complementary convention (true exactly when the count is divisible by m) would define the same circuit classes: a complemented MOD_m gate feeds its consumers through negated edges.

Main definitions

• AndOrModOp — AND, OR, and MOD_m operations
• AndOrModOp.eval — their evaluation on n input bits
• Basis.unboundedAndOrMod — the unbounded-fan-in AND/OR/MOD_m basis
• Basis.andOrToAndOrModHom — every AND/OR gate is an AND/OR/MOD_m gate

inductive Complexity.AndOrModOp : Type

Operations of the AND/OR/MOD_m basis. Negation is handled by per-input flags on gates.

• andOr (op : AndOrOp) : AndOrModOp

  An unbounded AND or OR operation.

• mod : AndOrModOp

  The MOD_m operation: true iff the number of true inputs is not divisible by m.

def Complexity.instReprAndOrModOp.repr : AndOrModOp → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Complexity.instReprAndOrModOp : Repr AndOrModOp

Equations

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

@[instance_reducible]

instance Complexity.instDecidableEqAndOrModOp : DecidableEq AndOrModOp

Equations

• Complexity.instDecidableEqAndOrModOp = Complexity.instDecidableEqAndOrModOp.decEq

def Complexity.instDecidableEqAndOrModOp.decEq (x✝ x✝¹ : AndOrModOp) : Decidable (x✝ = x✝¹)

Equations

• Complexity.instDecidableEqAndOrModOp.decEq (Complexity.AndOrModOp.andOr a) (Complexity.AndOrModOp.andOr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Complexity.instDecidableEqAndOrModOp.decEq (Complexity.AndOrModOp.andOr op) Complexity.AndOrModOp.mod = isFalse ⋯
• Complexity.instDecidableEqAndOrModOp.decEq Complexity.AndOrModOp.mod (Complexity.AndOrModOp.andOr op) = isFalse ⋯
• Complexity.instDecidableEqAndOrModOp.decEq Complexity.AndOrModOp.mod Complexity.AndOrModOp.mod = isTrue ⋯

def Complexity.AndOrModOp.eval (m : ℕ) : AndOrModOp → (n : ℕ) → BitString n → Bool

Evaluate an AND/OR/MOD_m operation on n input bits. AND and OR use AndOrOp.eval; MOD_m outputs true exactly when the number of true inputs is not divisible by m.

Equations

• Complexity.AndOrModOp.eval m (Complexity.AndOrModOp.andOr op) x✝¹ x✝ = op.eval x✝¹ x✝
• Complexity.AndOrModOp.eval m Complexity.AndOrModOp.mod x✝¹ x✝ = decide (Fin.countP x✝ % m ≠ 0)

def Complexity.Basis.unboundedAndOrMod (m : ℕ) : Basis

The basis of unbounded-fan-in AND, OR, and MOD_m gates. Negation is free (per-input flags on gates).

Equations

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

def Complexity.Basis.andOrToAndOrModHom (m : ℕ) : unboundedAndOr.Hom (unboundedAndOrMod m)

Every unbounded AND/OR gate is an AND/OR/MOD_m gate with the same semantics.

Equations

• Complexity.Basis.andOrToAndOrModHom m = { mapOp := fun (op : Complexity.Basis.unboundedAndOr.Op) (x : ℕ) => Complexity.AndOrModOp.andOr op, mapArity := ⋯, eval_map := ⋯ }