Computability

Part of the dependency closure of the small undecidable group constructions.

def Undecidability.wordOfNat (n k : ℕ) : Word n

A total computable enumeration of all words on n generators.

Equations

• Undecidability.wordOfNat n k = (Encodable.decode k).getD []

theorem Undecidability.wordOfNat_computable (n : ℕ) : Computable (wordOfNat n)

@[simp]

theorem Undecidability.wordOfNat_encode {n : ℕ} (w : Word n) : wordOfNat n (Encodable.encode w) = w

theorem Undecidability.not_computablePred_of_manyOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → Prop} {q : β → Prop} (hp : ¬ComputablePred p) (hred : p ≤₀ q) : ¬ComputablePred q

Undecidability transfers forward along a computable many-one reduction.

theorem Undecidability.isAdianRabinFamily_of_wordProblem_reduction {n m n' m' : ℕ} (P : FP n m) (R : Word n → FP n' m') (hP : ¬ComputablePred P.wordProblem) (hR : Computable₂ fun (w : Word n) (i : Fin m') => (R w).relator i) (hiff : ∀ (w : Word n), (R w).presentsTrivial ↔ P.wordProblem w) : FP.IsAdianRabinFamily fun (j : ℕ) => R (wordOfNat n j)

Turn a uniform word-indexed presentation construction into a natural-number indexed Adian--Rabin family.