TuringEquivalent — Mathlib

English

Two partial functions f and g are Turing equivalent if each is Turing reducible to the other.

Русский

Две частичные функции f и g эквивалентны по Тьюрингу, если каждая из них сводится к другой.

LaTeX

$$$ \text{abbrev } \text{TuringEquivalent } (f g : \mathbb{N} \to^. \mathbb{N}) : Prop := f \equiv_T g \iff (f ≤_T g) \land (g ≤_T f) $$$

Lean4

/-- `f` is Turing equivalent to `g` if `f` is reducible to `g` and `g` is reducible to `f`.
-/
abbrev TuringEquivalent (f g : ℕ →. ℕ) : Prop :=
  AntisymmRel TuringReducible f g

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