turingReducible — Mathlib

English

If a function f is partial recursive, then f ≤ᵀ g for every g (i.e., every partial function g).

Русский

Если функция f частично рекурсивна, то f сводима к любой функции g (то есть f ≤ᵀ g для любой g).

LaTeX

$$$ \forall {f g : \mathbb{N} \to^. \mathbb{N}},\ Nat.Partrec f \rightarrow TuringReducible f g $$$

Lean4

/-- If a function is partial recursive, then it is recursive in every partial function.
-/
theorem turingReducible (pF : Nat.Partrec f) : f ≤ᵀ g := by
  induction pF with
    repeat { constructor
    }
  | pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact RecursiveIn.prec ih₁ ih₂
  | rfind _ ih => exact RecursiveIn.rfind ih

Похожие утверждения