Combinational circuits

References

• [N. D. Belnap, A Useful Four-Valued Logic][Belnap1977]
• [Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits][Ghica2025]

@[reducible, inline]

abbrev Circuit.CombinationalCircuit : Type

The combinational circuit category over Belnap levels and Belnap gates.

Equations

• Circuit.CombinationalCircuit = Circuit.CombinationalCircuitCategory Circuit.BelnapLevel Circuit.BelnapGate

@[reducible, inline]

abbrev Circuit.CombinationalCircuit.and : OfNat.ofNat 2 ⟶ 1

The AND gate as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.and = Circuit.and

@[simp]

theorem Circuit.CombinationalCircuit.and_def (x y : Bool) : ↑and #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && y)]

@[reducible, inline]

abbrev Circuit.CombinationalCircuit.or : OfNat.ofNat 2 ⟶ 1

The OR gate as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.or = Circuit.or

@[simp]

theorem Circuit.CombinationalCircuit.or_def (x y : Bool) : ↑or #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x || y)]

@[reducible, inline]

abbrev Circuit.CombinationalCircuit.not : OfNat.ofNat 1 ⟶ 1

The NOT gate as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.not = Circuit.not

@[simp]

theorem Circuit.CombinationalCircuit.not_def (x : Bool) : ↑not #v[WithBotTop.coe x] = #v[WithBotTop.coe !x]

@[reducible, inline]

abbrev Circuit.CombinationalCircuit.nand : OfNat.ofNat 2 ⟶ 1

The NAND gate as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.nand = Circuit.nand

@[simp]

theorem Circuit.CombinationalCircuit.nand_def (x y : Bool) : ↑nand #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe !(x && y)]

@[reducible, inline]

abbrev Circuit.CombinationalCircuit.nor : OfNat.ofNat 2 ⟶ 1

The NOR gate as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.nor = Circuit.nor

@[simp]

theorem Circuit.CombinationalCircuit.nor_def (x y : Bool) : ↑nor #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe !(x || y)]

@[reducible, inline]

abbrev Circuit.CombinationalCircuit.fork : OfNat.ofNat 1 ⟶ 2

The fork (wire duplication) as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.fork = Circuit.CircuitCategory.fork

@[simp]

theorem Circuit.CombinationalCircuit.fork_def (x : Bool) : ↑fork #v[WithBotTop.coe x] = #v[WithBotTop.coe x, WithBotTop.coe x]

def Circuit.CombinationalCircuit.fork₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj (OfNat.ofNat 1) (OfNat.ofNat 1) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj 2 2

Two forks in parallel, duplicating each of two input wires.

Equations

• Circuit.CombinationalCircuit.fork₂ = CategoryTheory.MonoidalCategoryStruct.tensorHom Circuit.CombinationalCircuit.fork Circuit.CombinationalCircuit.fork

@[simp]

theorem Circuit.CombinationalCircuit.fork₂_def (x y : Bool) : ↑fork₂ #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe x, WithBotTop.coe x, WithBotTop.coe y, WithBotTop.coe y]

def Circuit.CombinationalCircuit.copy : OfNat.ofNat 2 ⟶ 4

Duplicate a pair of input wires, interleaving so the output is [x, y, x, y].

Equations

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

@[simp]

theorem Circuit.CombinationalCircuit.copy_def (x y : Bool) : ↑copy #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe x, WithBotTop.coe y, WithBotTop.coe x, WithBotTop.coe y]

def Circuit.CombinationalCircuit.xor : OfNat.ofNat 2 ⟶ 1

The XOR gate as a combinational circuit.

Equations

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

@[simp]

theorem Circuit.CombinationalCircuit.xor_def (x y : Bool) : ↑xor #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && !y || !x && y)]

def Circuit.CombinationalCircuit.xnor : OfNat.ofNat 2 ⟶ 1

The XNOR gate as a combinational circuit.

Equations

• Circuit.CombinationalCircuit.xnor = CategoryTheory.CategoryStruct.comp Circuit.CombinationalCircuit.xor Circuit.CombinationalCircuit.not

@[simp]

theorem Circuit.CombinationalCircuit.xnor_def (x y : Bool) : ↑xnor #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && y || !x && !y)]

def Circuit.CombinationalCircuit.halfAdder : OfNat.ofNat 2 ⟶ 2

A half adder, returning the sum and carry of two input bits.

Equations

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

@[simp]

theorem Circuit.CombinationalCircuit.halfAdder_def (x y : Bool) : ↑halfAdder #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && !y || !x && y), WithBotTop.coe (x && y)]

def Circuit.CombinationalCircuit.adder : OfNat.ofNat 3 ⟶ 2

A full adder built from two half adders, returning the sum and carry of three input bits.

Equations

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

@[simp]

theorem Circuit.CombinationalCircuit.adder_def (x y z : Bool) : ↑adder #v[WithBotTop.coe x, WithBotTop.coe y, WithBotTop.coe z] = #v[WithBotTop.coe ((x && !y || !x && y) && !z || !(x && !y || !x && y) && z), WithBotTop.coe (x && y || (x && !y || !x && y) && z)]