Circuit families

A circuit has a fixed number of inputs, while the words of a language have every length, so a language is decided by a family of circuits, one for each input length. The circuit on n inputs only has to handle the words of length n, the slice L.slice n of the language, and nothing relates the circuits for different lengths: families are a nonuniform model of computation.

The letters of a word are fed to the circuit as values of the carrier, and the single output letter is read as a verdict by a function accept into Bool. A language is decidable within a size bound s when some family decides it with at most s n gates on n inputs, exactly at every length. Over a carrier Bool read by id, this is a bound on the complexity of every slice. The classes SIZE and P/poly of the literature, over the De Morgan basis, are in Cslib.Computability.Circuit.Boolean.Family.

@[reducible, inline]

abbrev Cslib.Circuits.CircuitFamily (σ : Signature) : Type v

A family of single-output circuits, one for each number of inputs.

Equations

• Cslib.Circuits.CircuitFamily σ = ((n : ℕ) → Cslib.Circuits.Circuit σ n 1)

def Cslib.Circuits.CircuitFamily.Decides {σ : Signature} {α : Type u} (F : CircuitFamily σ) (I : Interpretation σ α) (accept : α → Bool) (L : Language α) : Prop

A circuit family decides L under I when, for every n, reading the output of its circuit on n inputs through accept gives the slice of L at length n.

Equations

• F.Decides I accept L = ∀ (n : ℕ) (x : Fin n → α), accept ((F n).eval I x 0) = L.slice n x

def Cslib.Circuits.DecidableInSize {σ : Signature} {α : Type u} (L : Language α) (I : Interpretation σ α) (accept : α → Bool) (s : ℕ → ℕ) : Prop

A language is decidable within the size bound s by circuits over I when some family decides it, reading outputs through accept, with at most s n gates on n inputs.

Equations

• Cslib.Circuits.DecidableInSize L I accept s = ∃ (F : Cslib.Circuits.CircuitFamily σ), F.Decides I accept L ∧ ∀ (n : ℕ), (F n).size ≤ s n

theorem Cslib.Circuits.CircuitFamily.decides_iff {σ : Signature} {α : Type u} {F : CircuitFamily σ} {I : Interpretation σ α} {accept : α → Bool} {L : Language α} : F.Decides I accept L ↔ ∀ (n : ℕ) (x : Fin n → α), accept ((F n).eval I x 0) = true ↔ List.ofFn x ∈ L

theorem Cslib.Circuits.DecidableInSize.mono {σ : Signature} {α : Type u} {I : Interpretation σ α} {accept : α → Bool} {L : Language α} {s s' : ℕ → ℕ} (h : DecidableInSize L I accept s) (hs : ∀ (n : ℕ), s n ≤ s' n) : DecidableInSize L I accept s'

The size bound can be weakened.

theorem Cslib.Circuits.decidableInSize_iff_exists_ecomplexity_le {σ : Signature} {α : Type u} {I : Interpretation σ α} {accept : α → Bool} {L : Language α} {s : ℕ → ℕ} : DecidableInSize L I accept s ↔ ∀ (n : ℕ), ∃ (f : (Fin n → α) → α), accept ∘ f = L.slice n ∧ (ecomplexity I fun (x : Fin n → α) (x_1 : Fin 1) => f x) ≤ ↑(s n)

A language is decidable within s exactly when each slice is accept of some function of extended complexity at most the bound.

Boolean carrier

Over the carrier Bool, reading the output by id makes the circuit compute the slice itself.

theorem Cslib.Circuits.CircuitFamily.decides_id_iff {σ : Signature} {F : CircuitFamily σ} {I : Interpretation σ Bool} {L : Language Bool} : F.Decides I id L ↔ ∀ (n : ℕ), (F n).Computes I fun (x : Fin n → Bool) (x_1 : Fin 1) => L.slice n x

theorem Cslib.Circuits.decidableInSize_id_iff_ecomplexity_le {σ : Signature} {s : ℕ → ℕ} {I : Interpretation σ Bool} {L : Language Bool} : DecidableInSize L I id s ↔ ∀ (n : ℕ), (ecomplexity I fun (x : Fin n → Bool) (x_1 : Fin 1) => L.slice n x) ≤ ↑(s n)

Over the carrier Bool, a language is decidable within s exactly when every slice has extended complexity at most the bound, so a slice with no circuit keeps the language out.

theorem Cslib.Circuits.decidableInSize_id_iff_complexity_le {σ : Signature} {s : ℕ → ℕ} {I : Interpretation σ Bool} {L : Language Bool} [I.IsComplete] : DecidableInSize L I id s ↔ ∀ (n : ℕ), (complexity I fun (x : Fin n → Bool) (x_1 : Fin 1) => L.slice n x) ≤ s n

Over a complete basis on Bool, a language is decidable within s exactly when every slice has complexity at most the bound.