Recursive isomorphism and 1-equivalence

DefinitionRecursively isomorphic predicates#✓fully proved

Two predicates \(P\) and \(Q\) on \(\mathbb{N}\) are recursively isomorphic when there is a computable bijection \(f : \mathbb{N} \to \mathbb{N}\) such that for every \(n\), \(P(n)\) holds if and only if \(Q(f(n))\) holds.

def RecursiveIsomorphic (P Q : ℕ → Prop) : Prop :=
  ∃ f : ℕ → ℕ, Computable f ∧ Function.Bijective f ∧ ∀ n, P n ↔ Q (f n)
Sources
  • Soare, Recursively Enumerable Sets and Degrees, Ch. I, Definition 7.1.
Used by 1
Used byA recursive isomorphism gives a 1-equivalence

TheoremThe inverse of a computable bijection is computable#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{N}\) be a computable bijection. Then its inverse function \(f^{-1} : \mathbb{N} \to \mathbb{N}\) is computable.

The inverse is computed by unbounded search for the unique preimage.

theorem computable_invFun_of_bijective {f : ℕ → ℕ} (hf : Computable f)
    (hbij : Function.Bijective f) : Computable (Function.invFun f)
Sources
  • Rogers, Theory of Recursive Functions and Effective Computability, §1.6 (inverses of recursive permutations).
Used by 1
Used byA recursive isomorphism gives a 1-equivalence

TheoremA recursive isomorphism gives a 1-equivalence#✓fully proved

Let \(P\) and \(Q\) be predicates on \(\mathbb{N}\). If \(P\) and \(Q\) are recursively isomorphic, then they are 1-equivalent: \(P\) is one-one reducible to \(Q\) and \(Q\) is one-one reducible to \(P\). Here \(P\) is one-one reducible to \(Q\) when there is a computable injective function \(g : \mathbb{N} \to \mathbb{N}\) such that for every \(n\), \(P(n)\) holds if and only if \(Q(g(n))\) holds.

This is the easy direction of Myhill's isomorphism theorem.

theorem recursiveIsomorphic_to_oneOneEquiv {P Q : ℕ → Prop}
    (h : RecursiveIsomorphic P Q) : OneOneEquiv P Q
Sources
  • Soare, Recursively Enumerable Sets and Degrees, Ch. I, Theorem 7.1.
Uses 2
Statement usesRecursively isomorphic predicates
Proof usesThe inverse of a computable bijection is computable
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.