Slices of languages

A language is the union of its slices, one for each word length. The slice at length n is a Boolean-valued function of the n letters of a word, so it can be handled by models of computation with a fixed number of inputs, such as circuits. Conversely, one such function for each length assembles into a language, and slicing that language recovers the functions.

Membership in an arbitrary language is not decidable, so a slice is defined classically. This is what lets notions defined for Boolean-valued functions, such as circuit complexity, apply to every language rather than only to decidable ones.

noncomputable def Language.slice {α : Type u_1} (L : Language α) (n : ℕ) : (Fin n → α) → Bool

The words of length n in L, as a Boolean-valued function of their letters.

Equations

• L.slice n x = decide (List.ofFn x ∈ L)

@[simp]

theorem Language.slice_eq_true_iff {α : Type u_1} {L : Language α} {n : ℕ} {x : Fin n → α} : L.slice n x = true ↔ List.ofFn x ∈ L

def Language.ofSlices {α : Type u_1} (f : (n : ℕ) → (Fin n → α) → Bool) : Language α

The language whose slice at each length n is f n.

Equations

• Language.ofSlices f = {w : List α | (f w.length fun (i : Fin w.length) => w[i]) = true}

@[simp]

theorem Language.slice_ofSlices {α : Type u_1} (f : (n : ℕ) → (Fin n → α) → Bool) (n : ℕ) : (ofSlices f).slice n = f n