Encodings for Uniform RE Computability Properties

This helper file provides concrete language views of Nat.Partrec.Code for the uniform computability predicates used by the RE decidability files.

def partrecCodeDomainLanguageOf (c : Nat.Partrec.Code) : Language Unit

The domain language of a partial-recursive code, represented over Unit.

The word length is the program input.

Equations

• partrecCodeDomainLanguageOf c w = (c.eval w.length).Dom

def partrecCodeGraphLanguageOf (c : Nat.Partrec.Code) : Language (ℕ × ℕ)

The graph language of a partial-recursive code.

Only singleton words are meaningful: [(n, y)] means that the code returns y on input n.

Equations

• partrecCodeGraphLanguageOf c [(n, y)] = (y ∈ c.eval n)
• partrecCodeGraphLanguageOf c x✝ = False

theorem partrecCodeDomainLanguage_empty_iff (c : Nat.Partrec.Code) : partrecCodeDomainLanguageOf c = ∅ ↔ ∀ (n : ℕ), ¬(c.eval n).Dom

theorem partrecCodeDomainLanguage_universal_iff (c : Nat.Partrec.Code) : partrecCodeDomainLanguageOf c = Set.univ ↔ ∀ (n : ℕ), (c.eval n).Dom

theorem partrecCodeGraphLanguage_eq_iff (p : Nat.Partrec.Code × Nat.Partrec.Code) : partrecCodeGraphLanguageOf p.1 = partrecCodeGraphLanguageOf p.2 ↔ p.1.eval = p.2.eval