Rice–Shapiro theorem

TheoremRice–Shapiro, upward closure#✓fully proved

In a class with a recognizable index set, every partial recursive extension of a partial recursive member is a member.

theorem rice_shapiro_mono (C : Set (ℕ →. ℕ)) (hC : TM2Recognizable fun c : Code ↦ c.eval ∈ C)
    {f g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (hfC : f ∈ C)
    (hfg : ∀ x, ∀ y ∈ f x, y ∈ g x) : g ∈ C

Uses 4 · Used by 1

Statement usesRecognizability by multi-stack machines

Proof usesThe halting problem is not co-recognizable by multi-stack machines · Recognizability transfers along mapping reductions · Parametrized s-m-n theorem

Used byEffective Rice–Shapiro, necessity

TheoremRice–Shapiro, finite approximation#✓fully proved

Every partial recursive member of a class with a recognizable index set has a partial recursive finite subfunction in the class.

theorem rice_shapiro_finite (C : Set (ℕ →. ℕ)) (hC : TM2Recognizable fun c : Code ↦ c.eval ∈ C)
    {f : ℕ →. ℕ} (hf : Nat.Partrec f) (hfC : f ∈ C) :
    ∃ θ : ℕ →. ℕ, Nat.Partrec θ ∧ (∀ x, ∀ y ∈ θ x, y ∈ f x) ∧ θ.Dom.Finite ∧ θ ∈ C

Uses 4 · Used by 1

Statement usesRecognizability by multi-stack machines

Proof usesThe halting problem is not co-recognizable by multi-stack machines · Recognizability transfers along mapping reductions · Parametrized s-m-n theorem

Used byEffective Rice–Shapiro, necessity

DefinitionFinite function of a list of pairs#✓fully proved

For a finite list \(\theta\) of pairs of natural numbers, the finite function of \(\theta\) is the partial function \(\mathbb{N} \rightharpoonup \mathbb{N}\) whose value at \(x\) is the second component of the first pair in \(\theta\) with first component \(x\), and which is undefined at \(x\) when \(\theta\) has no pair with first component \(x\).

def finFun (θ : List (ℕ × ℕ)) : ℕ →. ℕ := fun x ↦
  ((θ.filterMap fun p ↦ if p.1 = x then some p.2 else none).head? : Part ℕ)

Used by 4

Used byEffective Rice–Shapiro, necessity · Finite-domain partial functions are finite functions · Graphs of finite functions · Being a graph is recursively enumerable

DefinitionGraphs of finite functions#✓fully proved

A finite list \(\theta\) of pairs of natural numbers is a graph when, for every pair \((x, y)\) in \(\theta\), the finite function of \(\theta\) takes the value \(y\) at \(x\); that is, the first pair in \(\theta\) with first component \(x\) is \((x, y)\).

def IsGraph (θ : List (ℕ × ℕ)) : Prop := ∀ p ∈ θ, p.2 ∈ finFun θ p.1

Uses 1 · Used by 3

Statement usesFinite function of a list of pairs

Used byEffective Rice–Shapiro, necessity · Being a graph is recursively enumerable · The effective Rice–Shapiro theorem

TheoremBeing a graph is recursively enumerable#✓fully proved

The set of finite lists of pairs of natural numbers that are graphs is recursively enumerable.

This set is in fact decidable.

theorem rePred_isGraph : REPred IsGraph

Uses 3 · Used by 1

Statement usesGraphs of finite functions

Proof usesFinite function of a list of pairs · Bounded universal quantification preserves recursive enumerability

Used byEffective Rice–Shapiro, necessity

TheoremFinite-domain partial functions are finite functions#✓fully proved

For every partial function \(g : \mathbb{N} \rightharpoonup \mathbb{N}\) with finite domain there is a finite list \(\theta\) of pairs of natural numbers such that the finite function of \(\theta\) is \(g\) and, for every pair \((x, y)\) in \(\theta\), \(g(x)\) is defined and equals \(y\).

theorem exists_finFun_eq {g : ℕ →. ℕ} (hg : g.Dom.Finite) :
    ∃ θ : List (ℕ × ℕ), finFun θ = g ∧ ∀ p ∈ θ, p.2 ∈ g p.1

Uses 1 · Used by 1

Statement usesFinite function of a list of pairs

Used byEffective Rice–Shapiro, necessity

TheoremExtending a finite list of pairs is recursively enumerable#✓fully proved

The set of pairs \((c, \theta)\), where \(c\) is a code of a partial recursive function and \(\theta\) is a finite list of pairs of natural numbers, such that for every pair \((x, y)\) in \(\theta\) the function computed by \(c\) is defined at \(x\) with value \(y\), is recursively enumerable.

theorem rePred_subgraph :
    REPred fun q : Code × List (ℕ × ℕ) ↦ ∀ p ∈ q.2, p.2 ∈ q.1.eval p.1

Uses 2 · Used by 1

Proof usesExistential projection preserves recursive enumerability · Bounded universal quantification preserves recursive enumerability

Used byEffective Rice–Shapiro, sufficiency

TheoremEffective Rice–Shapiro, sufficiency#✓fully proved

Let \(C\) be a class of partial functions \(\mathbb{N} \rightharpoonup \mathbb{N}\) and let \(B\) be a recognizable set of finite lists of pairs of natural numbers. Suppose that a partial recursive function \(f\) is in \(C\) if and only if some \(\theta \in B\) satisfies: for every pair \((x, y)\) in \(\theta\), \(f(x)\) is defined and equals \(y\). Then the index set of \(C\), the set of codes \(c\) of partial recursive functions such that the function computed by \(c\) is in \(C\), is recognizable.

theorem tm2Recognizable_of_basis (C : Set (ℕ →. ℕ)) {B : List (ℕ × ℕ) → Prop}
    (hB : TM2Recognizable B)
    (hC : ∀ f : ℕ →. ℕ, Nat.Partrec f → (f ∈ C ↔ ∃ θ, B θ ∧ ∀ p ∈ θ, p.2 ∈ f p.1)) :
    TM2Recognizable fun c : Code ↦ c.eval ∈ C

Uses 5 · Used by 1

Statement usesRecognizability by multi-stack machines

Proof usesExtending a finite list of pairs is recursively enumerable · Multi-stack recognizable predicates are exactly the r.e. predicates · Recursively enumerable predicates are closed under conjunction · Existential projection preserves recursive enumerability

Used byThe effective Rice–Shapiro theorem

TheoremEffective Rice–Shapiro, necessity#✓fully proved

Let \(C\) be a class of partial functions \(\mathbb{N} \rightharpoonup \mathbb{N}\) whose index set, the set of codes \(c\) of partial recursive functions such that the function computed by \(c\) is in \(C\), is recognizable. Then there is a recognizable set \(B\) of finite lists of pairs of natural numbers, each of which is a graph, such that a partial recursive function \(f\) is in \(C\) if and only if some \(\theta \in B\) satisfies: for every pair \((x, y)\) in \(\theta\), \(f(x)\) is defined and equals \(y\).

theorem exists_basis_of_tm2Recognizable (C : Set (ℕ →. ℕ))
    (hC : TM2Recognizable fun c : Code ↦ c.eval ∈ C) :
    ∃ B : List (ℕ × ℕ) → Prop, TM2Recognizable B ∧ (∀ θ, B θ → IsGraph θ) ∧
      ∀ f : ℕ →. ℕ, Nat.Partrec f → (f ∈ C ↔ ∃ θ, B θ ∧ ∀ p ∈ θ, p.2 ∈ f p.1)

Uses 11 · Used by 1

Statement usesGraphs of finite functions · Recognizability by multi-stack machines

Proof usesFinite-domain partial functions are finite functions · Finite function of a list of pairs · Being a graph is recursively enumerable · Rice–Shapiro, finite approximation · Rice–Shapiro, upward closure · Multi-stack recognizable predicates are exactly the r.e. predicates · Recognizability transfers along mapping reductions · Recursively enumerable predicates are closed under conjunction · Parametrized s-m-n theorem

Used byThe effective Rice–Shapiro theorem

TheoremThe effective Rice–Shapiro theorem#✓fully proved

A class of partial functions has a recognizable index set iff, among partial recursive functions, its members are exactly the extensions of the finite functions in some recognizable set of graphs.

theorem tm2Recognizable_iff_exists_basis (C : Set (ℕ →. ℕ)) :
    TM2Recognizable (fun c : Code ↦ c.eval ∈ C) ↔
      ∃ B : List (ℕ × ℕ) → Prop, TM2Recognizable B ∧ (∀ θ, B θ → IsGraph θ) ∧
        ∀ f : ℕ →. ℕ, Nat.Partrec f → (f ∈ C ↔ ∃ θ, B θ ∧ ∀ p ∈ θ, p.2 ∈ f p.1)

Uses 4

Statement usesGraphs of finite functions · Recognizability by multi-stack machines

Proof usesEffective Rice–Shapiro, necessity · Effective Rice–Shapiro, sufficiency

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.