Circuits over the full basis

The full basis of arity k contains every constant and every operation with k arguments. Each takes one gate, and so does every operation with at most k arguments: a nullary operation is a constant, and other operations repeat their arguments to fill all k positions. Applying such an operation to r functions synthesized with budgets cost i therefore takes at most ∑ i, cost i + 1 gates. Synthesis.full_binary states the binary case with two separate budgets. All constructions preserve previously available functions.

Consequently, the full basis of arity k simulates any interpretation whose operations have arity at most k, replacing each operation by one gate. This includes nullary operations and the case k = 0, and needs no assumption on the carrier.

On a finite carrier, every full basis of arity at least two is functionally complete. The idea is disjunctive normal form: a function on a finite carrier is a finite table, so a circuit can find the row that matches its input and return that row's value. For each row, binary gates compare the input with the row one coordinate at a time, giving the row's value on a match and a fixed default otherwise. Further binary gates merge these answers by keeping the one that differs from the default. Over Bool with default false, this is exactly disjunctive normal form. Larger arities follow by simulation.

theorem Cslib.Circuits.Synthesis.full_const {U : Type u} {k n : ℕ} {s : Set ((Fin n → U) → U)} (value : U) : Synthesis fullInterpretation s {fun (x : Fin n → U) => value} 1

A constant can be synthesized with one gate of the full basis.

theorem Cslib.Circuits.Synthesis.full_gate {U : Type u} {k n : ℕ} {s : Set ((Fin n → U) → U)} {r : ℕ} (hr : r ≤ k) (op : (Fin r → U) → U) (args : Fin r → (Fin n → U) → U) (hargs : ∀ (i : Fin r), args i ∈ s) : Synthesis fullInterpretation s {fun (x : Fin n → U) => op fun (i : Fin r) => args i x} 1

Apply any operation with at most k arguments to available functions using one gate. Nullary operations use a constant gate; other operations pad their arguments by repetition.

theorem Cslib.Circuits.Synthesis.full_gate_of_syntheses {U : Type u} {k n : ℕ} {s : Set ((Fin n → U) → U)} {r : ℕ} (hr : r ≤ k) (op : (Fin r → U) → U) (args : Fin r → (Fin n → U) → U) (cost : Fin r → ℕ) (h : ∀ (i : Fin r), Synthesis fullInterpretation s {args i} (cost i)) : Synthesis fullInterpretation s {fun (x : Fin n → U) => op fun (i : Fin r) => args i x} (∑ i : Fin r, cost i + 1)

Construct the arguments of an operation of arity at most k, then apply it with one further gate. All functions computed while constructing the arguments remain available.

theorem Cslib.Circuits.Synthesis.full_binary {U : Type u} {n a b : ℕ} {s : Set ((Fin n → U) → U)} {f g : (Fin n → U) → U} (hf : Synthesis fullInterpretation s {f} a) (hg : Synthesis fullInterpretation s {g} b) (op : U → U → U) : Synthesis fullInterpretation s {fun (x : Fin n → U) => op (f x) (g x)} (a + b + 1)

Apply any binary operation to synthesized functions in the binary full basis.

theorem Cslib.Circuits.fullInterpretation_simulatesWithCost {U : Type u} {k : ℕ} {σ : Signature} (I : Interpretation σ U) (h : ∀ (op : σ.Op), σ.Arity op ≤ k) : fullInterpretation.SimulatesWithCost I fun (x : σ.Op) => 1

The full basis simulates operations of arity at most k with a budget of one gate each.

theorem Cslib.Circuits.fullInterpretation_simulates {U : Type u} {k : ℕ} {σ : Signature} (I : Interpretation σ U) (h : ∀ (op : σ.Op), σ.Arity op ≤ k) : fullInterpretation.Simulates I

The full basis simulates any interpretation whose operations have arity at most k.

theorem Cslib.Circuits.fullInterpretation_isComplete {U : Type u} {k : ℕ} [Finite U] (hk : 2 ≤ k) : fullInterpretation.IsComplete

Every full basis of arity at least two is complete on a finite carrier.

instance Cslib.Circuits.instIsCompleteFullInterpretation {U : Type u} {k : ℕ} [Finite U] : fullInterpretation.IsComplete

Full bases with at least two arguments are complete on finite carriers.