TuringReducible — Mathlib

English

Let f,g : ℕ →. ℕ be partial functions. Then f is Turing reducible to g if f is computable with oracle g (i.e., f ≤ᵀ g).

Русский

Пусть f,g : ℕ →. ℕ — частичные функции. Тогда f выводима относительно ордора g (f ≤ᵀ g).

LaTeX

$$$ \text{abbrev } \text{TuringReducible } (f g : \mathbb{N} \to^. \mathbb{N}) : Prop := \text{RecursiveIn } \{ g \} f $$$

Lean4

/-- `f` is Turing reducible to `g` if `f` is partial recursive given access to the oracle `g`
-/
abbrev TuringReducible (f g : ℕ →. ℕ) : Prop :=
  RecursiveIn { g } f

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