Decidable and recognizable predicates
TheoremComputable predicates are closed under conjunction#✓fully proved
Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). If \(p\) and \(q\) are computable predicates on \(\alpha\), then the predicate \(a \mapsto p(a) \land q(a)\) is computable.
theorem ComputablePred.and {p q : α → Prop} (hp : ComputablePred p) (hq : ComputablePred q) :
ComputablePred fun a ↦ p a ∧ q aTheoremComputable predicates are closed under disjunction#✓fully proved
Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). If \(p\) and \(q\) are computable predicates on \(\alpha\), then the predicate \(a \mapsto p(a) \lor q(a)\) is computable.
theorem ComputablePred.or {p q : α → Prop} (hp : ComputablePred p) (hq : ComputablePred q) :
ComputablePred fun a ↦ p a ∨ q aTheoremRecursively enumerable predicates are closed under conjunction#✓fully proved
Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). If \(p\) and \(q\) are recursively enumerable predicates on \(\alpha\), then the predicate \(a \mapsto p(a) \land q(a)\) is recursively enumerable.
The proof runs one semi-decision procedure, then the other.
Used by 8
TheoremRecursively enumerable predicates are closed under disjunction#✓fully proved
Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). If \(p\) and \(q\) are recursively enumerable predicates on \(\alpha\), then the predicate \(a \mapsto p(a) \lor q(a)\) is recursively enumerable.
The proof runs both semi-decision procedures in parallel.
Used by 1
TheoremBounded existential quantification preserves recursive enumerability#✓fully proved
Let \(\alpha\) and \(\beta\) be types with primitive recursive encodings into \(\mathbb{N}\), let \(R\) be a relation between \(\alpha\) and \(\beta\) that is recursively enumerable as a predicate on pairs \((a, b)\), and let \(c\) be a primitive recursive function sending each \(a \in \alpha\) to a finite list \(c(a)\) of elements of \(\beta\). Then the predicate \(a \mapsto \exists b \in c(a),\ R(a, b)\) is recursively enumerable.
The proof is by dovetailing: it searches for a step bound \(k\) at which the simulation of the semi-decision procedure for \(R\) halts on \((a, b)\) for some \(b\) in \(c(a)\).
theorem REPred.exists_mem {β : Type*} [Primcodable β] {R : α → β → Prop}
(hR : REPred fun p : α × β ↦ R p.1 p.2) {c : α → List β} (hc : Primrec c) :
REPred fun a ↦ ∃ b ∈ c a, R a bTheoremBounded universal quantification preserves recursive enumerability#✓fully proved
Let \(\alpha\) and \(\beta\) be types with primitive recursive encodings into \(\mathbb{N}\), let \(R\) be a relation between \(\alpha\) and \(\beta\) that is recursively enumerable as a predicate on pairs \((a, b)\), and let \(c\) be a primitive recursive function sending each \(a \in \alpha\) to a finite list \(c(a)\) of elements of \(\beta\). Then the predicate \(a \mapsto \forall b \in c(a),\ R(a, b)\) is recursively enumerable.
The proof searches for one step bound \(k\) at which the simulation of the semi-decision procedure for \(R\) halts on \((a, b)\) for every \(b\) in \(c(a)\); the step-bounded simulation is monotone in \(k\).
theorem REPred.forall_mem {β : Type*} [Primcodable β] {R : α → β → Prop}
(hR : REPred fun p : α × β ↦ R p.1 p.2) {c : α → List β} (hc : Primrec c) :
REPred fun a ↦ ∀ b ∈ c a, R a bTheoremSearching a computable list with a computable test is computable#✓fully proved
Let \(\gamma\) and \(\beta\) be types with primitive recursive encodings into \(\mathbb{N}\), let \(l\) be a computable function sending each \(x \in \gamma\) to a finite list \(l(x)\) of elements of \(\beta\), and let \(g\) be a computable Boolean-valued function of \(x \in \gamma\) and \(b \in \beta\). Then the Boolean-valued function that sends \(x\) to true exactly when \(g(x, b)\) is true for some \(b\) in \(l(x)\) is computable.
The proof scans the indices of \(l(x)\) by primitive recursion.
theorem computable_list_any {γ β : Type*} [Primcodable γ] [Primcodable β]
{l : γ → List β} {g : γ → β → Bool} (hl : Computable l) (hg : Computable₂ g) :
Computable fun x ↦ (l x).any (g x)Used by 1
TheoremSelection for r.e. relations#✓fully proved
Let \(\alpha\) and \(\beta\) be types with primitive recursive encodings into \(\mathbb{N}\), and let \(R\) be a relation between \(\alpha\) and \(\beta\) that is recursively enumerable as a predicate on pairs \((a, b)\). Then there is a partial recursive function \(g\) from \(\alpha\) to \(\beta\) such that, for every \(a \in \alpha\), if \(g(a)\) is defined then its value \(b\) satisfies \(R(a, b)\), and \(g(a)\) is defined whenever some \(b \in \beta\) satisfies \(R(a, b)\).
The proof searches over pairs of a candidate \(b\) and a step bound by dovetailing with the step-bounded simulation of the semi-decision procedure for \(R\).
theorem REPred.exists_partrec_choose {β : Type*} [Primcodable β] {R : α → β → Prop}
(hR : REPred fun p : α × β ↦ R p.1 p.2) :
∃ g : α →. β, Partrec g ∧ (∀ a b, b ∈ g a → R a b) ∧ ∀ a, (∃ b, R a b) → (g a).DomTheoremExistential projection preserves recursive enumerability#✓fully proved
Let \(\alpha\) and \(\beta\) be types with primitive recursive encodings into \(\mathbb{N}\), and let \(R\) be a relation between \(\alpha\) and \(\beta\) that is recursively enumerable as a predicate on pairs \((a, b)\). Then the predicate \(a \mapsto \exists b \in \beta,\ R(a, b)\) is recursively enumerable.
The predicate is the domain of the partial recursive function that selects a witness of \(R\).
theorem REPred.exists {β : Type*} [Primcodable β] {R : α → β → Prop}
(hR : REPred fun p : α × β ↦ R p.1 p.2) : REPred fun a ↦ ∃ b, R a bUses 1 · Used by 14
DefinitionDecidability by multi-stack machines#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is decidable by a multi-stack machine when there is a function \(f : \mathbb{N} \to \mathbb{N}\) computed by a multi-stack Turing machine, with input and output numbers written in binary, such that for every \(a \in \alpha\), \(f(\mathrm{encode}(a)) = 1\) if and only if \(p(a)\).
def TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aUsed by 68
DefinitionRecognizability by multi-stack machines#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is recognizable by a multi-stack machine when there are a multi-stack Turing machine \(M\) and an identification of its input alphabet with the Booleans such that for every \(a \in \alpha\), \(p(a)\) holds if and only if \(M\) halts when started on the binary word of \(\mathrm{encode}(a)\).
def TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)def TM2HaltsOn (tm : FinTM2) (l : List (tm.Γ tm.k₀)) : Prop :=
(StateTransition.eval tm.step (initList tm l)).DomMathlibExt/Computability/TuringMachine/Recursive/Halts.lean:50
Uses 1 · Used by 40
DefinitionCo-recognizability by multi-stack machines#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is co-recognizable by a multi-stack machine when its complement \(\neg p\) is recognizable by a multi-stack machine.
def TM2CoRecognizable (p : α → Prop) : Prop := TM2Recognizable fun a ↦ ¬p adef TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
Uses 1 · Used by 13
TheoremMulti-stack decidable predicates are exactly the computable predicates#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is decidable by a multi-stack machine if and only if it is computable, that is, \(p\) is decidable and its Boolean characteristic function \(\alpha \to \mathrm{Bool}\) is computable.
theorem tm2Decidable_iff_computablePred {p : α → Prop} :
TM2Decidable p ↔ ComputablePred pdef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
Uses 3 · Used by 37
TheoremMulti-stack recognizable predicates are exactly the r.e. predicates#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is recognizable by a multi-stack machine if and only if it is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(p\) holds is partial recursive.
theorem tm2Recognizable_iff_rePred {p : α → Prop} : TM2Recognizable p ↔ REPred pdef TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
Uses 4 · Used by 21
TheoremMulti-stack co-recognizable predicates are exactly the co-r.e. predicates#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is co-recognizable by a multi-stack machine if and only if its complement \(\neg p\) is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(\neg p\) holds is partial recursive.
theorem tm2CoRecognizable_iff_rePred_not {p : α → Prop} :
TM2CoRecognizable p ↔ REPred fun a ↦ ¬p adef TM2CoRecognizable (p : α → Prop) : Prop := TM2Recognizable fun a ↦ ¬p aCSLibExt/Computability/Decidability/Basic.lean:70
Uses 2 · Used by 5
TheoremDecidable predicates are recognizable by multi-stack machines#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a multi-stack machine, then \(p\) is recognizable by a multi-stack machine.
theorem TM2Decidable.tm2Recognizable {p : α → Prop} (h : TM2Decidable p) : TM2Recognizable pdef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
def TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
TheoremDecidability by multi-stack machines is closed under complement#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a multi-stack machine, then so is its complement \(\neg p\).
theorem TM2Decidable.not {p : α → Prop} (h : TM2Decidable p) : TM2Decidable fun a ↦ ¬p adef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
Uses 2 · Used by 3
TheoremDecidable predicates are co-recognizable by multi-stack machines#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a multi-stack machine, then \(p\) is co-recognizable by a multi-stack machine, that is, its complement \(\neg p\) is recognizable by a multi-stack machine.
theorem TM2Decidable.tm2CoRecognizable {p : α → Prop} (h : TM2Decidable p) :
TM2CoRecognizable pdef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
def TM2CoRecognizable (p : α → Prop) : Prop := TM2Recognizable fun a ↦ ¬p aCSLibExt/Computability/Decidability/Basic.lean:70
TheoremPost's theorem for multi-stack machines#✓fully proved
Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is decidable by a multi-stack machine if and only if it is both recognizable and co-recognizable by a multi-stack machine.
theorem tm2Decidable_iff_tm2Recognizable_and_tm2CoRecognizable {p : α → Prop} :
TM2Decidable p ↔ TM2Recognizable p ∧ TM2CoRecognizable pdef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
def TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
def TM2CoRecognizable (p : α → Prop) : Prop := TM2Recognizable fun a ↦ ¬p aCSLibExt/Computability/Decidability/Basic.lean:70
Uses 6 · Used by 2
TheoremDecidable predicates are closed under conjunction#✓fully proved
Let \(p\) and \(q\) be predicates on a type \(\alpha\) with a primitive recursive encoding. If \(p\) and \(q\) are both decidable by multi-stack machines, then so is the predicate \(a \mapsto p(a) \wedge q(a)\).
theorem TM2Decidable.and {p q : α → Prop} (hp : TM2Decidable p) (hq : TM2Decidable q) :
TM2Decidable fun a ↦ p a ∧ q adef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
TheoremDecidable predicates are closed under disjunction#✓fully proved
Let \(\alpha\) be a type with a primitive recursive encoding. If \(p\) and \(q\) are predicates on \(\alpha\) that are decidable by a multi-stack Turing machine, then so is the predicate \(a \mapsto p(a) \lor q(a)\).
theorem TM2Decidable.or {p q : α → Prop} (hp : TM2Decidable p) (hq : TM2Decidable q) :
TM2Decidable fun a ↦ p a ∨ q adef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
TheoremRecognizable predicates are closed under conjunction#✓fully proved
Let \(p\) and \(q\) be predicates on a type \(\alpha\) with a primitive recursive encoding. If \(p\) and \(q\) are both recognizable by multi-stack machines, then so is the predicate \(a \mapsto p(a) \wedge q(a)\).
theorem TM2Recognizable.and {p q : α → Prop} (hp : TM2Recognizable p) (hq : TM2Recognizable q) :
TM2Recognizable fun a ↦ p a ∧ q adef TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
TheoremRecognizable predicates are closed under disjunction#✓fully proved
Let \(\alpha\) be a type with a primitive recursive encoding. If \(p\) and \(q\) are predicates on \(\alpha\) that are recognizable by a multi-stack Turing machine, then so is the predicate \(a \mapsto p(a) \lor q(a)\).
theorem TM2Recognizable.or {p q : α → Prop} (hp : TM2Recognizable p) (hq : TM2Recognizable q) :
TM2Recognizable fun a ↦ p a ∨ q adef TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
DefinitionLanguage of a Boolean test#✓fully proved
For a Boolean-valued function \(f\) on words over an alphabet \(\sigma\), the language of \(f\) is the set of words \(u\) over \(\sigma\) with \(f(u) = \mathrm{true}\).
TheoremMembership in a concatenation of languages#✓fully proved
For languages \(L_1\) and \(L_2\) over an alphabet \(\sigma\) and a word \(w\) over \(\sigma\), \(w\) lies in the concatenation \(L_1 L_2\) if and only if there are words \(u\) and \(v\) with \(w = uv\), \(u \in L_1\) and \(v \in L_2\).
DefinitionBounded split test#✓fully proved
Given Boolean tests \(f\) and \(g\) on words over \(\sigma\), a word \(w\) and a natural number \(n\), the split test is the Boolean value that is true exactly when there is some \(i < n\) such that \(f\) is true on the prefix of \(w\) of length \(\min(i, |w|)\) and \(g\) is true on the remaining suffix of \(w\).
def splitTest (f g : List σ → Bool) (w : List σ) (n : ℕ) : Bool :=
Nat.rec false (fun i acc ↦ acc || (f (w.take i) && g (w.drop i))) nUsed by 1
TheoremDecidable languages have computable membership tests#✓fully proved
Let \(L\) be a language over an alphabet \(\sigma\) with a primitive recursive encoding. If membership in \(L\) is decidable by a multi-stack machine, then there is a computable function \(f\) from words over \(\sigma\) to Booleans such that \(L\) is the language of \(f\), that is, the set of words \(u\) with \(f(u) = \mathrm{true}\).
theorem TM2Decidable.exists_computable {L : Language σ} (h : TM2Decidable (· ∈ L)) :
∃ f : List σ → Bool, Computable f ∧ L = boolLang fdef TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
def boolLang (f : List σ → Bool) : Language σ := {u | f u = true}CSLibExt/Computability/Decidability/Closure.lean:81
Uses 3 · Used by 2
TheoremDecidable languages are closed under concatenation#✓fully proved
Let \(\sigma\) be an alphabet with a primitive recursive encoding. If \(L_1\) and \(L_2\) are languages over \(\sigma\) whose membership predicates are decidable by a multi-stack Turing machine, then the membership predicate of their concatenation \(L_1 L_2 = \{uv : u \in L_1, v \in L_2\}\) is also decidable by a multi-stack Turing machine.
theorem TM2Decidable.mul {L₁ L₂ : Language σ} (h₁ : TM2Decidable (· ∈ L₁))
(h₂ : TM2Decidable (· ∈ L₂)) : TM2Decidable (· ∈ L₁ * L₂)def TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
DefinitionSplits of a word#✓fully proved
For a word \(w\) over \(\sigma\) of length \(n\), this is the list of the \(n + 1\) pairs \((u, v)\) of words with \(uv = w\), ordered by the length of \(u\): for each \(i = 0, 1, \dots, n\) it contains the prefix of \(w\) of length \(i\) paired with the remaining suffix.
def splits (w : List σ) : List (List σ × List σ) :=
(List.range (w.length + 1)).map fun i ↦ (w.take i, w.drop i)Used by 1
TheoremRecognizable languages are closed under concatenation#✓fully proved
Let \(L_1\) and \(L_2\) be languages over an alphabet \(\sigma\) with a primitive recursive encoding. If membership in \(L_1\) and membership in \(L_2\) are recognizable by multi-stack machines, then so is membership in the concatenation \(L_1 L_2\), the set of words \(uv\) with \(u \in L_1\) and \(v \in L_2\).
theorem TM2Recognizable.mul {L₁ L₂ : Language σ} (h₁ : TM2Recognizable (· ∈ L₁))
(h₂ : TM2Recognizable (· ∈ L₂)) : TM2Recognizable (· ∈ L₁ * L₂)def TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
Uses 6
DefinitionExtending a list of pieces by a letter#✓fully proved
Given a letter \(a\) and a list \(\pi = [u_1, \dots, u_k]\) of words, the extensions of \(\pi\) by \(a\) are listed as follows: first \([[a], u_1, \dots, u_k]\), which starts a new piece \([a]\), and then, only when \(k \ge 1\), also \([a u_1, u_2, \dots, u_k]\), which puts the letter \(a\) in front of the first piece.
DefinitionPartitions of a word into nonempty factors#✓fully proved
For a word \(w\) over \(\sigma\), this is the list of all ways to write \(w\) as a concatenation \(w = u_1 u_2 \cdots u_k\) of nonempty words \(u_1, \dots, u_k\), each recorded as the list \([u_1, \dots, u_k]\). The empty word has exactly one such partition, the empty list.
def partitions (w : List σ) : List (List (List σ)) :=
w.foldr (fun a acc ↦ acc.flatMap (extendPartitions a)) [[]]def extendPartitions (a : σ) (ws : List (List σ)) : List (List (List σ)) :=
([a] :: ws) :: ws.head?.elim [] fun u ↦ [(a :: u) :: ws.tail]CSLibExt/Computability/Decidability/Closure.lean:198
Uses 1 · Used by 2
TheoremRecognizable languages are closed under Kleene star#✓fully proved
Let \(L\) be a language over an alphabet \(\sigma\) with a primitive recursive encoding. If membership in \(L\) is recognizable by a multi-stack machine, then so is membership in the Kleene star \(L^*\), the set of all concatenations \(u_1 \cdots u_k\) with \(k \ge 0\) and \(u_1, \dots, u_k \in L\).
theorem TM2Recognizable.kstar {L : Language σ} (h : TM2Recognizable (· ∈ L)) :
TM2Recognizable (· ∈ L∗)def TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
Uses 6
TheoremDecidable languages are closed under Kleene star#✓fully proved
Let \(L\) be a language over an alphabet \(\sigma\) with a primitive recursive encoding. If membership in \(L\) is decidable by a multi-stack machine, then so is membership in the Kleene star \(L^*\), the set of all concatenations \(u_1 \cdots u_k\) with \(k \ge 0\) and \(u_1, \dots, u_k \in L\).
theorem TM2Decidable.kstar {L : Language σ} (h : TM2Decidable (· ∈ L)) :
TM2Decidable (· ∈ L∗)def TM2Decidable (p : α → Prop) : Prop :=
∃ f : ℕ → ℕ, Nonempty (TM2Computable encodeNat encodeNat f) ∧ ∀ a, f (encode a) = 1 ↔ p aCSLibExt/Computability/Decidability/Basic.lean:60
Uses 7
TheoremRecognizable languages are closed under alphabet maps#✓fully proved
Let \(\sigma\) and \(\tau\) be alphabets with primitive recursive encodings, let \(f : \sigma \to \tau\) be primitive recursive, and let \(L\) be a language over \(\sigma\). If membership in \(L\) is recognizable by a multi-stack machine, then so is membership in the image language \(f(L) = \{f(a_1) \cdots f(a_n) : a_1 \cdots a_n \in L\}\), obtained by applying \(f\) letter by letter to the words of \(L\).
The recognizer searches for a preimage word by unbounded dovetailing. Every map between finite alphabets is primitive recursive.
theorem TM2Recognizable.map {τ : Type*} [Primcodable τ] {f : σ → τ} (hf : Primrec f)
{L : Language σ} (h : TM2Recognizable (· ∈ L)) :
TM2Recognizable (· ∈ Language.map f L)def TM2Recognizable (p : α → Prop) : Prop :=
∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
∀ a, p a ↔ TM2HaltsOn tm ((encodeNat (encode a)).map e.symm)CSLibExt/Computability/Decidability/Basic.lean:65
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.