Enumerators

DefinitionEnumerating a predicate#✓fully proved

For a type \(\alpha\) with a primitive recursive encoding, a function \(e\) assigning to each natural number \(n\) either an element \(e(n)\) of \(\alpha\) or nothing enumerates a predicate \(p\) on \(\alpha\) when, for every \(a \in \alpha\), \(p(a)\) holds if and only if \(e(n) = a\) for some natural number \(n\).

def Enumerates (e : ℕ → Option α) (p : α → Prop) : Prop := ∀ a, p a ↔ ∃ n, e n = some a

Used by 3

Used byRecognizable languages are enumerable · Recognizable languages are exactly the enumerable ones · Enumerable languages are recognizable

TheoremRecognizable languages are enumerable#✓fully proved

For every type \(\alpha\) with a primitive recursive encoding and every predicate \(p\) on \(\alpha\) that is recognizable by a multi-stack machine, there is a computable function \(e\), assigning to each natural number either an element of \(\alpha\) or nothing, that enumerates \(p\).

theorem TM2Recognizable.exists_enumerator {p : α → Prop} (h : TM2Recognizable p) :
    ∃ e : ℕ → Option α, Computable e ∧ Enumerates e p

Uses 3 · Used by 1

Statement usesEnumerating a predicate · Recognizability by multi-stack machines

Proof usesMulti-stack recognizable predicates are exactly the r.e. predicates

Used byRecognizable languages are exactly the enumerable ones

TheoremEnumerable languages are recognizable#✓fully proved

For every type \(\alpha\) with a primitive recursive encoding, every predicate \(p\) on \(\alpha\) and every computable function \(e\), assigning to each natural number either an element of \(\alpha\) or nothing, that enumerates \(p\), the predicate \(p\) is recognizable by a multi-stack machine.

theorem tm2Recognizable_of_enumerates {p : α → Prop} {e : ℕ → Option α} (he : Computable e)
    (hep : Enumerates e p) : TM2Recognizable p

Uses 3 · Used by 1

Statement usesEnumerating a predicate · Recognizability by multi-stack machines

Proof usesMulti-stack recognizable predicates are exactly the r.e. predicates

Used byRecognizable languages are exactly the enumerable ones

TheoremRecognizable languages are exactly the enumerable ones#✓fully proved

For every type \(\alpha\) with a primitive recursive encoding, a predicate \(p\) on \(\alpha\) is recognizable by a multi-stack machine if and only if some computable function \(e\), assigning to each natural number either an element of \(\alpha\) or nothing, enumerates \(p\). This is Sipser, Theorem 3.21: a language is Turing-recognizable if and only if some enumerator enumerates it.

theorem tm2Recognizable_iff_exists_enumerator {p : α → Prop} :
    TM2Recognizable p ↔ ∃ e : ℕ → Option α, Computable e ∧ Enumerates e p

Uses 4

Statement usesEnumerating a predicate · Recognizability by multi-stack machines

Proof usesRecognizable languages are enumerable · Enumerable languages are recognizable

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.