The dual-rail translation of De Morgan circuits

A De Morgan circuit becomes a monotone circuit by computing, for every wire, both its value and its negation [Gol77]. The monotone circuit (Cslib.Circuits.Monotone.dualRail) has 2 n + 1 inputs: input 0 is the constant true, and the input i of the De Morgan circuit is carried positively by input 2 i + 1 and negatively by input 2 i + 2 (railBits). Each gate is replaced by two gates, carrying it positively and negatively: an AND gate by the AND of the positive rails and the OR of the negative rails, an OR gate dually, a negation by copies of the crossed rails (conjunctions with the constant true wire), and a constant by the constant and its negation (dualGates). Every wire w of the De Morgan circuit is then carried by the wires 2 w + 1 and 2 w + 2 (railWire), uniformly for inputs and gates, so the translation of a gate depends on the gate alone, not on its position.

The translation works on gate lists (dualCode): it keeps well-formedness (isCodeFrom_dualCode), and evaluating the translated list on the dual-rail inputs gives the dual-rail values (evalCode_dualCode). The translated circuit computes the same function on the dual-rail inputs (eval_dualRail) and has twice the size (size_dualRail).

Main definitions

• Cslib.Circuits.Monotone.railWire, Cslib.Circuits.Monotone.railBits: the dual-rail wires and inputs.
• Cslib.Circuits.Monotone.dualGates, Cslib.Circuits.Monotone.dualCode: the translation of gates and gate lists.
• Cslib.Circuits.Monotone.dualRail: the dual-rail translation of a De Morgan circuit.

Main results

• Cslib.Circuits.Monotone.evalCode_dualCode: the translated gate list computes the dual-rail values.
• Cslib.Circuits.Monotone.eval_dualRail: the translated circuit computes the same function.
• Cslib.Circuits.Monotone.size_dualRail: the translated circuit has twice the size.

References

• L. M. Goldschlager, The monotone and planar circuit value problems are log space complete for P

Dual-rail wires and inputs

def Cslib.Circuits.Monotone.railWire (b : Bool) (w : ℕ) : ℕ

The wire carrying wire w positively (b = true), 2 w + 1, or negatively, 2 w + 2. Wire 0 is the constant true.

def Cslib.Circuits.Monotone.railBits (x : List Bool) : List Bool

The dual-rail values: the constant true, then each value followed by its negation.

@[simp]

theorem Cslib.Circuits.Monotone.length_railBits (x : List Bool) : (railBits x).length = 2 * x.length + 1

theorem Cslib.Circuits.Monotone.railBits_append (x : List Bool) (v : Bool) : railBits (x ++ [v]) = railBits x ++ [v, !v]

@[simp]

theorem Cslib.Circuits.Monotone.getD_railBits_zero (x : List Bool) : (railBits x).getD 0 false = true

@[simp]

theorem Cslib.Circuits.Monotone.getElem_railBits_zero (x : List Bool) (h : 0 < (railBits x).length) : (railBits x)[0] = true

theorem Cslib.Circuits.Monotone.getD_railBits_true (x : List Bool) {w : ℕ} (hw : w < x.length) : (railBits x).getD (railWire true w) false = x.getD w false

The positive rail of a value.

theorem Cslib.Circuits.Monotone.getD_railBits_false (x : List Bool) {w : ℕ} (hw : w < x.length) : (railBits x).getD (railWire false w) false = !x.getD w false

The negative rail of a value.

Gates

def Cslib.Circuits.Monotone.dualGates (g : Boolean.Op × List ℕ) : List (Op × List ℕ)

The two monotone gates computing a De Morgan gate positively and negatively, from its operation and its wires g.2: an AND gate by the AND of the positive rails and the OR of the negative rails, an OR gate dually, a negation by the crossed rails (each in a conjunction with the constant true wire 0), a constant by the constant and its negation.

@[simp]

theorem Cslib.Circuits.Monotone.length_dualGates (g : Boolean.Op × List ℕ) : (dualGates g).length = 2

def Cslib.Circuits.Monotone.dualCode (gates : List (Boolean.Op × List ℕ)) : List (Op × List ℕ)

The dual-rail translation of a gate list: each gate by its two monotone gates.

@[simp]

theorem Cslib.Circuits.Monotone.length_dualCode (gates : List (Boolean.Op × List ℕ)) : (dualCode gates).length = 2 * gates.length

theorem Cslib.Circuits.Monotone.dualCode_append (gates gates' : List (Boolean.Op × List ℕ)) : dualCode (gates ++ gates') = dualCode gates ++ dualCode gates'

theorem Cslib.Circuits.Monotone.isCodeFrom_dualCode {n k : ℕ} {gates : List (Boolean.Op × List ℕ)} : Program.IsCodeFrom Boolean.signature n k gates → Program.IsCodeFrom signature (2 * n + 1) (2 * k) (dualCode gates)

The translation keeps well-formedness: the gates of a De Morgan gate list reading the first n + k wires become gates reading the first 2 n + 1 + 2 k wires.

theorem Cslib.Circuits.Monotone.evalCode_dualCode (x : List Bool) {gates : List (Boolean.Op × List ℕ)} (h : Program.IsCodeFrom Boolean.signature x.length 0 gates) : evalCode interpretation false (railBits x) (dualCode gates) = railBits (evalCode Boolean.interpretation false x gates)

The translated gate list computes the dual-rail values: on the dual-rail inputs, the gates translating gate j carry the value of gate j and its negation.

Circuits

def Cslib.Circuits.Monotone.railBitString {n : ℕ} (x : BitString n) : BitString (2 * n + 1)

The dual-rail inputs of an input of a De Morgan circuit (railBits).

theorem Cslib.Circuits.Monotone.ofFn_railBitString {n : ℕ} (x : BitString n) : List.ofFn (railBitString x) = railBits (List.ofFn x)

theorem Cslib.Circuits.Monotone.isSome_ofCode_dualRail {n m : ℕ} (c : Circuit Boolean.signature n m) : (Circuit.ofCode (2 * n + 1) m (dualCode c.code.1, List.map (railWire true) c.code.2)).isSome = true

def Cslib.Circuits.Monotone.dualRail {n m : ℕ} (c : Circuit Boolean.signature n m) : Circuit signature (2 * n + 1) m

The dual-rail translation of a De Morgan circuit: a monotone circuit on the 2 n + 1 dual-rail inputs with two gates for every gate.

theorem Cslib.Circuits.Monotone.code_dualRail {n m : ℕ} (c : Circuit Boolean.signature n m) : (dualRail c).code = (dualCode c.code.1, List.map (railWire true) c.code.2)

theorem Cslib.Circuits.Monotone.size_dualRail {n m : ℕ} (c : Circuit Boolean.signature n m) : (dualRail c).size = 2 * c.size

The dual-rail translation has twice the size.

theorem Cslib.Circuits.Monotone.toNat_outputs_dualRail {n m : ℕ} (c : Circuit Boolean.signature n m) (j : Fin m) : ((dualRail c).outputs j).toNat = railWire true (c.outputs j).toNat

theorem Cslib.Circuits.Monotone.eval_dualRail {n m : ℕ} (c : Circuit Boolean.signature n m) (x : BitString n) (j : Fin m) : (dualRail c).eval interpretation (railBitString x) j = c.eval Boolean.interpretation x j

The dual-rail translation computes the same function on the dual-rail inputs.