CSLib circuits whose outputs are gates

A CSLib circuit (Cslib.Circuits.Circuit) may designate any wire as an output, including an original input, and designating outputs is free. Complexitylib's typed circuits instead end in M distinct output gates, each counted in the size. This file names the CSLib circuits whose every output is an internal gate Circuit.GatedOutputs.

Translating a typed circuit into CSLib's model gives a circuit with gated outputs and the same size (Complexity.Circuit.gatedOutputs_toStraightLine and Complexity.Circuit.size_toStraightLine, in Complexitylib.Circuits.StraightLine). Gated outputs alone do not make the two size conventions agree when there are several outputs: two outputs may name the same gate, and an output gate may feed later gates, neither of which a typed circuit allows. A gated CSLib circuit with two outputs can thus have a single gate, while a typed circuit with two outputs has at least two. The converse translation, from gated CSLib circuits back to typed circuits, is planned (docs/CircuitMigration.md, step 2.3) but not yet formalized, so this library proves no size comparison in that direction.

Sequential composition keeps this property when the outer circuit has it, and parallel composition keeps it when both circuits do. The number of outputs that forward an input, Circuit.inputOutputCount, measures how far a circuit is from having it.

This file lives in Complexitylib/Cslib/ because it extends CSLib types in their home namespace Cslib.Circuits; its contents are candidates for upstreaming to CSLib.

Main definitions

• Cslib.Circuits.Wire.IsGate — a wire is the output of an internal gate
• Cslib.Circuits.Wire.gateOf — the gate carrying a gate wire
• Cslib.Circuits.Circuit.GatedOutputs — every output is an internal gate
• Cslib.Circuits.Circuit.inputOutputCount — the number of outputs that forward an input

Main results

• Cslib.Circuits.Circuit.GatedOutputs.size_pos — a gated circuit with an output has a gate
• Cslib.Circuits.Circuit.GatedOutputs.comp, Cslib.Circuits.Circuit.GatedOutputs.append — composition keeps gated outputs
• Cslib.Circuits.Circuit.inputOutputCount_eq_zero_iff — no output forwards an input exactly when the outputs are gated

def Cslib.Circuits.Wire.IsGate {n g : ℕ} : Wire n g → Prop

Whether a wire is the output of an internal gate rather than an original input.

Equations

• (Cslib.Circuits.Wire.input input).IsGate = False
• (Cslib.Circuits.Wire.gate gate).IsGate = True

@[instance_reducible]

instance Cslib.Circuits.Wire.instDecidableIsGate {n g : ℕ} (w : Wire n g) : Decidable w.IsGate

Whether a wire is a gate is decided by its constructor.

Equations

• (Cslib.Circuits.Wire.input input).instDecidableIsGate = isFalse ⋯
• (Cslib.Circuits.Wire.gate gate).instDecidableIsGate = isTrue trivial

@[simp]

theorem Cslib.Circuits.Wire.not_isGate_input {n g : ℕ} (i : Fin n) : ¬(input i).IsGate

An original input is not a gate.

@[simp]

theorem Cslib.Circuits.Wire.isGate_gate {n g : ℕ} (j : Fin g) : (gate j).IsGate

A gate wire is a gate.

theorem Cslib.Circuits.Wire.isGate_iff_exists {n g : ℕ} (w : Wire n g) : w.IsGate ↔ ∃ (j : Fin g), w = gate j

A wire is a gate exactly when it is gate j for some j.

@[simp]

theorem Cslib.Circuits.Wire.isGate_castSucc {n g : ℕ} (w : Wire n g) : w.castSucc.IsGate ↔ w.IsGate

Widening a wire into a longer program keeps whether it is a gate.

@[simp]

theorem Cslib.Circuits.Wire.isGate_castAdd {n k g : ℕ} (w : Wire n g) : (castAdd k w).IsGate ↔ w.IsGate

Continuing a program by further gates keeps whether a wire is a gate.

def Cslib.Circuits.Wire.gateOf {n g : ℕ} (w : Wire n g) : w.IsGate → Fin g

The gate carrying a gate wire. The input case is absurd, so this is computable.

Equations

• (Cslib.Circuits.Wire.gate j).gateOf x_2 = j
• (Cslib.Circuits.Wire.input input).gateOf h = False.elim h

@[simp]

theorem Cslib.Circuits.Wire.gateOf_gate {n g : ℕ} (j : Fin g) (h : (gate j).IsGate) : (gate j).gateOf h = j

The gate carrying gate j is j.

@[simp]

theorem Cslib.Circuits.Wire.gate_gateOf {n g : ℕ} (w : Wire n g) (h : w.IsGate) : gate (w.gateOf h) = w

A gate wire is the wire of the gate carrying it.

theorem Cslib.Circuits.Wire.IsGate.appendWire {n k g₁ g₂ : ℕ} {w : Wire k g₂} (h : w.IsGate) (feed : Fin k → Wire n g₁) : (Program.appendWire feed w).IsGate

A gate wire of a continued program's second part is a gate.

def Cslib.Circuits.Circuit.GatedOutputs {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Prop

Every designated output of c is an internal gate, never an original input. Typed circuits translate to circuits with this property and the same size (Complexity.Circuit.gatedOutputs_toStraightLine, Complexity.Circuit.size_toStraightLine). The property alone does not match CSLib's free outputs with the typed charge of one distinct gate per output: with several outputs, gated outputs may share a gate or feed later gates.

Equations

• c.GatedOutputs = ∀ (o : Fin m), (c.outputs o).IsGate

@[instance_reducible]

instance Cslib.Circuits.Circuit.instDecidableGatedOutputs {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Decidable c.GatedOutputs

Whether every output is a gate is decidable, output by output.

Equations

• c.instDecidableGatedOutputs = Fintype.decidableForallFintype

theorem Cslib.Circuits.Circuit.GatedOutputs.size_pos {σ : Signature} {n m : ℕ} [NeZero m] {c : Circuit σ n m} (h : c.GatedOutputs) : 0 < c.size

A gated circuit with an output has a gate.

theorem Cslib.Circuits.Circuit.GatedOutputs.comp {σ : Signature} {n m p : ℕ} {d : Circuit σ m p} (hd : d.GatedOutputs) (c : Circuit σ n m) : (d.comp c).GatedOutputs

Sequential composition keeps gated outputs when the outer circuit has them: its outputs are gates after the inner circuit's gates.

theorem Cslib.Circuits.Circuit.GatedOutputs.append {σ : Signature} {n m p : ℕ} {c : Circuit σ n m} {d : Circuit σ n p} (hc : c.GatedOutputs) (hd : d.GatedOutputs) : (c.append d).GatedOutputs

Parallel composition keeps gated outputs when both circuits have them.

def Cslib.Circuits.Circuit.inputOutputCount {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ℕ

The number of outputs of c that forward an original input instead of a gate.

Equations

• c.inputOutputCount = {o : Fin m | ¬(c.outputs o).IsGate}.card

theorem Cslib.Circuits.Circuit.inputOutputCount_eq_zero_iff {σ : Signature} {n m : ℕ} {c : Circuit σ n m} : c.inputOutputCount = 0 ↔ c.GatedOutputs

No output forwards an input exactly when the outputs are gated.

theorem Cslib.Circuits.Circuit.inputOutputCount_le {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.inputOutputCount ≤ m

At most every output forwards an input.