Replacing gates by constants

The signature σ.withConstants P is σ with a constant, an operation of arity zero, for every element of P, and I.withConstants γ interprets the constant k as γ k. Replacing gates of a program by constants (Program.replaceGates) keeps the shape of the program: the gate g becomes the constant k when r g = some k, and keeps its line when r g = none.

Erasing a set of special gates (Program.eraseGates) replaces each special gate g by a constant named after g itself, in σ.withConstants {g // special g}. The inner gates of the erased program are the inner gates that are not special (Program.innerGates_eraseGates), and its fan-in is that of the other gates (Program.fanInAtMost_eraseGates_iff). When the constants hold the values of the special gates in a run of the original program, the erased program has the same run (Program.trace_eraseGates). So a program with a few gates of unbounded fan-in is a program of bounded fan-in, once the values of those gates are given.

Main definitions

• Cslib.Circuits.Signature.withConstants, Cslib.Circuits.Interpretation.withConstants: a signature and an interpretation with constants added.
• Cslib.Circuits.Program.replaceGates: replacing some gates by constants.
• Cslib.Circuits.Program.eraseGates: replacing the special gates by constants named after them.

Main results

• Cslib.Circuits.Program.lines_eraseGates: the lines of the erased program.
• Cslib.Circuits.Program.innerGates_eraseGates: its inner gates are the ordinary inner gates.
• Cslib.Circuits.Program.fanInAtMost_eraseGates_iff: its fan-in is that of the ordinary gates.
• Cslib.Circuits.Program.trace_eraseGates_gate, Cslib.Circuits.Program.trace_eraseGates: its run, and the run with the true values of the special gates.

Constants

@[reducible, inline]

abbrev Cslib.Circuits.Signature.withConstants (σ : Signature) (P : Type w) : Signature

The signature σ with a constant, an operation of arity zero, for every element of P.

def Cslib.Circuits.Interpretation.withConstants {σ : Signature} {U : Type u_1} {P : Type w} (I : Interpretation σ U) (γ : P → U) : Interpretation (σ.withConstants P) U

The interpretation I, with the constant k holding the value γ k.

@[simp]

theorem Cslib.Circuits.Interpretation.withConstants_inl {σ : Signature} {U : Type u_1} {P : Type w} (I : Interpretation σ U) (γ : P → U) (o : σ.Op) (x : Fin (σ.Arity o) → U) : I.withConstants γ (Sum.inl o) x = I o x

@[simp]

theorem Cslib.Circuits.Interpretation.withConstants_inr {σ : Signature} {U : Type u_1} {P : Type w} (I : Interpretation σ U) (γ : P → U) (k : P) (x : Fin 0 → U) : I.withConstants γ (Sum.inr k) x = γ k

def Cslib.Circuits.Line.const {σ : Signature} {n s : ℕ} {P : Type w} (k : P) : Line (σ.withConstants P) n s

The line of the constant k.

def Cslib.Circuits.Line.liftConstants {σ : Signature} {n s : ℕ} {P : Type w} (line : Line σ n s) : Line (σ.withConstants P) n s

A line over σ, as a line over the signature with constants.

@[simp]

theorem Cslib.Circuits.Line.const_mapWires {σ : Signature} {n s : ℕ} {P : Type w} {n' s' : ℕ} (k : P) (f : Wire n s → Wire n' s') : (const k).mapWires f = const k

@[simp]

theorem Cslib.Circuits.Line.liftConstants_mapWires {σ : Signature} {n s : ℕ} {P : Type w} {n' s' : ℕ} (line : Line σ n s) (f : Wire n s → Wire n' s') : line.liftConstants.mapWires f = (line.mapWires f).liftConstants

Replacing gates by constants

def Cslib.Circuits.Program.replaceGates {σ : Signature} {n : ℕ} {P : Type w} {s : ℕ} : Program σ n s → (Fin s → Option P) → Program (σ.withConstants P) n s

Replacing gates by constants. The gate g becomes the constant k when r g = some k, and keeps its line when r g = none.

theorem Cslib.Circuits.Program.lines_replaceGates {σ : Signature} {n s : ℕ} {P : Type w} (p : Program σ n s) (r : Fin s → Option P) (g : Fin s) : (p.replaceGates r).lines g = (r g).elim (p.lines g).liftConstants Line.const

The lines of a program with gates replaced by constants.

Erasing the special gates

def Cslib.Circuits.Program.eraseGates {σ : Signature} {n s : ℕ} (special : Fin s → Prop) [DecidablePred special] (p : Program σ n s) : Program (σ.withConstants { g : Fin s // special g }) n s

Erasing the special gates. Each special gate g becomes the constant named g, and the other gates are kept.

theorem Cslib.Circuits.Program.lines_eraseGates {σ : Signature} {n s : ℕ} {special : Fin s → Prop} [DecidablePred special] (p : Program σ n s) (g : Fin s) : (eraseGates special p).lines g = if h : special g then Line.const ⟨g, h⟩ else (p.lines g).liftConstants

The lines of an erased program.

theorem Cslib.Circuits.Program.lines_eraseGates_of_special {σ : Signature} {n s : ℕ} {special : Fin s → Prop} [DecidablePred special] (p : Program σ n s) {g : Fin s} (hg : special g) : (eraseGates special p).lines g = Line.const ⟨g, hg⟩

theorem Cslib.Circuits.Program.lines_eraseGates_of_not_special {σ : Signature} {n s : ℕ} {special : Fin s → Prop} [DecidablePred special] (p : Program σ n s) {g : Fin s} (hg : ¬special g) : (eraseGates special p).lines g = (p.lines g).liftConstants

theorem Cslib.Circuits.Program.arity_lines_eraseGates {σ : Signature} {n s : ℕ} {special : Fin s → Prop} [DecidablePred special] (p : Program σ n s) (g : Fin s) : (σ.withConstants { g : Fin s // special g }).Arity ((eraseGates special p).lines g).op = if special g then 0 else σ.Arity (p.lines g).op

The arity of a gate of the erased program: zero for a special gate, and the arity of the gate otherwise.

theorem Cslib.Circuits.Program.innerGates_eraseGates {σ : Signature} {n s : ℕ} {special : Fin s → Prop} [DecidablePred special] (p : Program σ n s) : (eraseGates special p).innerGates = {g ∈ p.innerGates | ¬special g}

The inner gates of the erased program are the inner gates that are not special.

theorem Cslib.Circuits.Program.fanInAtMost_eraseGates_iff {σ : Signature} {n s : ℕ} {special : Fin s → Prop} [DecidablePred special] {p : Program σ n s} {r : ℕ} : (eraseGates special p).FanInAtMost r ↔ ∀ (g : Fin s), ¬special g → σ.Arity (p.lines g).op ≤ r

The erased program has fan-in at most r exactly when every gate that is not special does.

theorem Cslib.Circuits.Program.trace_eraseGates_gate {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {γ : { g : Fin s // special g } → U} (p : Program σ n s) (x : Fin n → U) (g : Fin s) : (eraseGates special p).trace (I.withConstants γ) x (Wire.gate g) = if h : special g then γ ⟨g, h⟩ else I (p.lines g).op fun (a : Fin (σ.Arity (p.lines g).op)) => (eraseGates special p).trace (I.withConstants γ) x ((p.lines g).wires a)

The value of a gate in a run of the erased program: the value of its constant for a special gate, and the gate applied to the values of its arguments otherwise.

theorem Cslib.Circuits.Program.trace_eraseGates {σ : Signature} {n s : ℕ} {U : Type u_1} {special : Fin s → Prop} [DecidablePred special] {I : Interpretation σ U} {γ : { g : Fin s // special g } → U} {p : Program σ n s} {x : Fin n → U} (hγ : ∀ (g : Fin s) (h : special g), γ ⟨g, h⟩ = p.trace I x (Wire.gate g)) : (eraseGates special p).trace (I.withConstants γ) x = p.trace I x

Erasing gates keeps the run when the constants hold the values of the special gates in the run of the original program.