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.and {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

The AND gate as a circuit morphism.

Equations

• Circuit.and = Circuit.CircuitCategory.gate Circuit.BelnapGate.and

@[reducible, inline]

abbrev Circuit.or {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

The OR gate as a circuit morphism.

Equations

• Circuit.or = Circuit.CircuitCategory.gate Circuit.BelnapGate.or

@[reducible, inline]

abbrev Circuit.not {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 1 ⟶ 1

The NOT gate as a circuit morphism.

Equations

• Circuit.not = Circuit.CircuitCategory.gate Circuit.BelnapGate.not

@[reducible, inline]

abbrev Circuit.nand {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

The NAND gate, built as AND followed by NOT.

Equations

• Circuit.nand = CategoryTheory.CategoryStruct.comp Circuit.and Circuit.not

@[reducible, inline]

abbrev Circuit.nor {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

The NOR gate, built as OR followed by NOT.

Equations

• Circuit.nor = CategoryTheory.CategoryStruct.comp Circuit.or Circuit.not