Translating circuits and formulas between signatures

A map of signatures φ : σ.Hom τ (Cslib.Circuits.Signature.Hom) sends each operation of σ to an operation of τ of the same arity. It is a map of the operation symbols, unlike cslib's Homomorphism, which maps the carriers of two interpretations of one signature. It translates programs and circuits over σ into programs and circuits over τ gate by gate (Circuit.mapOp), keeping the size and the depth (Circuit.size_mapOp, Circuit.depth_mapOp), and when φ keeps the meaning of every operation (Signature.Hom.Preserves) the translated circuit computes the same function (Circuit.eval_mapOp). This embeds circuits over a basis into circuits over a larger basis; it is analogous to cslib's Program.simulate with a budget of one gate for every operation. Formulas are translated likewise (Formula.mapOp), keeping their function, size, leaves and depth.

Main definitions

• Cslib.Circuits.Line.mapOp, Cslib.Circuits.Program.mapOp, Cslib.Circuits.Circuit.mapOp, Cslib.Circuits.Formula.mapOp: the translation along a map of signatures.

Main results

• Cslib.Circuits.Circuit.eval_mapOp, Cslib.Circuits.Circuit.Computes.mapOp: the translation computes the same function along a meaning-preserving map.
• Cslib.Circuits.Circuit.size_mapOp, Cslib.Circuits.Circuit.depth_mapOp: size and depth are kept.
• Cslib.Circuits.Circuit.mapOp_id, Cslib.Circuits.Circuit.mapOp_comp: translation is functorial.
• Cslib.Circuits.Formula.eval_mapOp, Cslib.Circuits.Formula.depthWith_mapOp: a translated formula computes the same function, with depth measured by the costs of the images.

def Cslib.Circuits.Line.mapOp {σ : Signature} {τ : Signature} {n g : ℕ} (φ : σ.Hom τ) (line : Line σ n g) : Line τ n g

The line performing φ op on the wires of line.

def Cslib.Circuits.Program.mapOp {σ : Signature} {τ : Signature} {n g : ℕ} (φ : σ.Hom τ) (p : Program σ n g) : Program τ n g

The program performing φ op in place of each operation op: its lines translated by Line.mapOp.

def Cslib.Circuits.Circuit.mapOp {σ : Signature} {τ : Signature} {n m : ℕ} (φ : σ.Hom τ) (c : Circuit σ n m) : Circuit τ n m

The circuit performing φ op in place of each operation op.

@[simp]

theorem Cslib.Circuits.Line.mapOp_op {σ : Signature} {τ : Signature} {n g : ℕ} {φ : σ.Hom τ} (line : Line σ n g) : (mapOp φ line).op = φ line.op

@[simp]

theorem Cslib.Circuits.Line.mapOp_wires {σ : Signature} {τ : Signature} {n g : ℕ} {φ : σ.Hom τ} (line : Line σ n g) (a : Fin (τ.Arity (φ line.op))) : (mapOp φ line).wires a = line.wires (Fin.cast ⋯ a)

@[simp]

theorem Cslib.Circuits.Program.mapOp_empty {σ : Signature} {τ : Signature} {n : ℕ} {φ : σ.Hom τ} : mapOp φ empty = empty

@[simp]

theorem Cslib.Circuits.Program.mapOp_gate {σ : Signature} {τ : Signature} {n g : ℕ} {φ : σ.Hom τ} (p : Program σ n g) (line : Line σ n g) : mapOp φ (p.gate line) = (mapOp φ p).gate (Line.mapOp φ line)

@[simp]

theorem Cslib.Circuits.Circuit.mapOp_program {σ : Signature} {τ : Signature} {n m : ℕ} {φ : σ.Hom τ} (c : Circuit σ n m) : (mapOp φ c).program = Program.mapOp φ c.program

@[simp]

theorem Cslib.Circuits.Circuit.mapOp_outputs {σ : Signature} {τ : Signature} {n m : ℕ} {φ : σ.Hom τ} (c : Circuit σ n m) : (mapOp φ c).outputs = c.outputs

@[simp]

theorem Cslib.Circuits.Program.fanInAtMost_mapOp {σ : Signature} {τ : Signature} {n g : ℕ} {φ : σ.Hom τ} (p : Program σ n g) (r : ℕ) : (mapOp φ p).FanInAtMost r ↔ p.FanInAtMost r

Translating operation symbols preserves every fan-in bound.

@[simp]

theorem Cslib.Circuits.Circuit.fanInAtMost_mapOp {σ : Signature} {τ : Signature} {n m : ℕ} {φ : σ.Hom τ} (c : Circuit σ n m) (r : ℕ) : (mapOp φ c).FanInAtMost r ↔ c.FanInAtMost r

Translating operation symbols preserves every circuit fan-in bound.

@[simp]

theorem Cslib.Circuits.Line.mapOp_id {σ : Signature} {n g : ℕ} (line : Line σ n g) : mapOp (Signature.Hom.id σ) line = line

theorem Cslib.Circuits.Line.mapOp_comp {σ : Signature} {τ : Signature} {υ : Signature} {n g : ℕ} {φ : σ.Hom τ} (ψ : τ.Hom υ) (line : Line σ n g) : mapOp (ψ.comp φ) line = mapOp ψ (mapOp φ line)

Translating a line along a composition translates it twice.

@[simp]

theorem Cslib.Circuits.Program.mapOp_id {σ : Signature} {n g : ℕ} (p : Program σ n g) : mapOp (Signature.Hom.id σ) p = p

theorem Cslib.Circuits.Program.mapOp_comp {σ : Signature} {τ : Signature} {υ : Signature} {n g : ℕ} {φ : σ.Hom τ} (ψ : τ.Hom υ) (p : Program σ n g) : mapOp (ψ.comp φ) p = mapOp ψ (mapOp φ p)

Translating a program along a composition translates it twice.

@[simp]

theorem Cslib.Circuits.Circuit.mapOp_id {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : mapOp (Signature.Hom.id σ) c = c

theorem Cslib.Circuits.Circuit.mapOp_comp {σ : Signature} {τ : Signature} {υ : Signature} {n m : ℕ} {φ : σ.Hom τ} (ψ : τ.Hom υ) (c : Circuit σ n m) : mapOp (ψ.comp φ) c = mapOp ψ (mapOp φ c)

Translating a circuit along a composition translates it twice.

@[simp]

theorem Cslib.Circuits.Circuit.size_mapOp {σ : Signature} {τ : Signature} {n m : ℕ} {φ : σ.Hom τ} (c : Circuit σ n m) : (mapOp φ c).size = c.size

theorem Cslib.Circuits.Line.depth_mapOp {σ : Signature} {τ : Signature} {n g : ℕ} {φ : σ.Hom τ} (line : Line σ n g) (depths : Wire n g → ℕ) : (mapOp φ line).depth depths = line.depth depths

A translated line has the same depth.

theorem Cslib.Circuits.Program.depths_mapOp {σ : Signature} {τ : Signature} {n g : ℕ} {φ : σ.Hom τ} (p : Program σ n g) : (mapOp φ p).depths = p.depths

The translated program has the same gate depths.

@[simp]

theorem Cslib.Circuits.Circuit.depth_mapOp {σ : Signature} {τ : Signature} {n m : ℕ} {φ : σ.Hom τ} (c : Circuit σ n m) : (mapOp φ c).depth = c.depth

theorem Cslib.Circuits.Program.eval_mapOp {σ : Signature} {τ : Signature} {n g : ℕ} {U : Type u_1} {φ : σ.Hom τ} {I : Interpretation σ U} {J : Interpretation τ U} [hφ : φ.Preserves I J] (p : Program σ n g) (x : Fin n → U) : (mapOp φ p).eval J x = p.eval I x

The translated program computes the same gate values along a meaning-preserving map.

theorem Cslib.Circuits.Circuit.eval_mapOp {σ : Signature} {τ : Signature} {n m : ℕ} {U : Type u_1} {φ : σ.Hom τ} {I : Interpretation σ U} {J : Interpretation τ U} [hφ : φ.Preserves I J] (c : Circuit σ n m) (x : Fin n → U) : (mapOp φ c).eval J x = c.eval I x

The translated circuit computes the same function along a meaning-preserving map.

theorem Cslib.Circuits.Circuit.Computes.mapOp {σ : Signature} {τ : Signature} {n m : ℕ} {U : Type u_1} {φ : σ.Hom τ} {I : Interpretation σ U} {J : Interpretation τ U} [φ.Preserves I J] {c : Circuit σ n m} {f : (Fin n → U) → Fin m → U} (hc : c.Computes I f) : (Circuit.mapOp φ c).Computes J f

A circuit translated along a meaning-preserving map computes what the circuit computes.

Formulas

def Cslib.Circuits.Formula.mapOp {σ : Signature} {τ : Signature} {n : ℕ} (φ : σ.Hom τ) : Formula σ n → Formula τ n

The formula performing φ op in place of each operation op.

@[simp]

theorem Cslib.Circuits.Formula.mapOp_input {σ : Signature} {τ : Signature} {n : ℕ} {φ : σ.Hom τ} (i : Fin n) : mapOp φ (input i) = input i

@[simp]

theorem Cslib.Circuits.Formula.mapOp_gate {σ : Signature} {τ : Signature} {n : ℕ} {φ : σ.Hom τ} (op : σ.Op) (args : Fin (σ.Arity op) → Formula σ n) : mapOp φ (gate op args) = gate (φ op) fun (a : Fin (τ.Arity (φ op))) => mapOp φ (args (Fin.cast ⋯ a))

@[simp]

theorem Cslib.Circuits.Formula.depthWith_mapOp {σ : Signature} {τ : Signature} {n : ℕ} {φ : σ.Hom τ} (cost : τ.Op → ℕ) (F : Formula σ n) : depthWith cost (mapOp φ F) = depthWith (cost ∘ ⇑φ) F

The translated formula has the same depth when φ op costs what op does.

@[simp]

theorem Cslib.Circuits.Formula.size_mapOp {σ : Signature} {τ : Signature} {n : ℕ} {φ : σ.Hom τ} (F : Formula σ n) : (mapOp φ F).size = F.size

The translated formula has the same size.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_mapOp {σ : Signature} {τ : Signature} {n : ℕ} {φ : σ.Hom τ} (F : Formula σ n) : (mapOp φ F).leafSize = F.leafSize

The translated formula has the same leaves.

theorem Cslib.Circuits.Formula.eval_mapOp {σ : Signature} {τ : Signature} {n : ℕ} {U : Type u_1} {φ : σ.Hom τ} {I : Interpretation σ U} {J : Interpretation τ U} [hφ : φ.Preserves I J] (F : Formula σ n) (x : Fin n → U) : (mapOp φ F).eval J x = F.eval I x

The translated formula computes the same function along a meaning-preserving map.

theorem Cslib.Circuits.Formula.Computes.mapOp {σ : Signature} {τ : Signature} {n : ℕ} {U : Type u_1} {φ : σ.Hom τ} {I : Interpretation σ U} {J : Interpretation τ U} [φ.Preserves I J] {F : Formula σ n} {f : (Fin n → U) → U} (hF : F.Computes I f) : (Formula.mapOp φ F).Computes J f

A formula translated along a meaning-preserving map computes what the formula computes.