General recursive equals Turing computable

turing_recursive_equiv — a formalization challenge from the lean-eval benchmark.

Notes

The Turing–Kleene equivalence (total form): a total function f : ℕ → ℕ is recursive (Computable) iff it is computed by some Turing machine (mathlib's FinTM2 model, TM2Computable) under the standard binary encoding encodeNat. Both sides are mathlib predicates but no theorem links them; the forward direction is essentially tr_eval plus plumbing, while the backward direction (TM-computable ⇒ recursive) is absent from mathlib. The total reading is used since general recursive is classically the total recursive functions and TM2Computable is total-only. Candidate from §23 of the Knill survey.

Formal statement

/-- **General recursive = Turing computable** (total form). A total function
`f : ℕ → ℕ` is recursive (`Computable`, i.e. partial recursive as a partial
function) **iff** it is computed by some Turing machine (mathlib's `FinTM2`
model) under the standard binary encoding of `ℕ`. This is Knill's class
equality; the backward direction (TM-computable ⇒ recursive) is absent from
mathlib. -/
theorem turing_recursive_equiv (f : ℕ → ℕ) :
    Computable f ↔ Nonempty (TM2Computable encodeNat encodeNat f) := by
  sorry

Informal solution sketch

Two inclusions. Recursive ⇒ TM-computable: by Nat.Partrec.Code.exists_code every Computable f is the evaluation of a partial recursive code; mathlib's Turing.PartrecToTM2.tr_eval constructively builds a TM2 machine evaluating any ToPartrec.Code, so composing the translations and verifying the encodeNat input/output encoding yields a TM2Computable witness. TM-computable ⇒ recursive: given a FinTM2 machine, its step relation is primitive recursive in the (finite) state and tape data, so the computation history and its halting time are recursive; running the machine until it halts and decoding the output exhibits f as obtained by composition and unbounded minimization over a primitive recursive predicate, hence Computable. This converse is the half missing from mathlib.

Source

A. M. Turing, On Computable Numbers (1936); S. C. Kleene, General recursive functions of natural numbers (1936). Knill, Some fundamental theorems in mathematics, §23.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: turing_recursive_equiv
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.