Elementary completeness of the De Morgan basis

Shannon expansion on the first input constructs a formula for every Boolean function. Compiling that formula gives a circuit, including for zero inputs. This elementary existence argument is independent of circuit counting, minimum complexity, and asymptotically efficient synthesis.

def Algebraic.DeMorgan.Expression.ofFunction {n : ℕ} : ScalarFunction Bool n → Expression n

A truth-table formula obtained by recursively selecting between the two restrictions of a Boolean function at its first input.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.Expression.ofFunction function = Algebraic.DeMorgan.Expression.constant (function Fin.elim0)

@[simp]

theorem Algebraic.DeMorgan.Expression.ofFunction_eval {n : ℕ} (function : ScalarFunction Bool n) (input : Fin n → Bool) : eval input (ofFunction function) = function input

Truth-table synthesis computes the supplied Boolean function.

theorem Algebraic.DeMorgan.exists_circuit {n : ℕ} (function : ScalarFunction Bool n) : ∃ (circuit : Circuit signature n 1), circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input

Every scalar Boolean function has a De Morgan circuit.

theorem Algebraic.DeMorgan.functionallyComplete : Interpretation.FunctionallyComplete interpretation

The De Morgan interpretation computes every finite-output Boolean target, including targets with no inputs or no outputs.