Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Every partial recursive function is computed by a Turing machine`

groundedproofs/Lax251941Proofs/Results.lean · lax-251941

What this proof establishes

no assumptions

thm✓Lax251941.TuringCompleteness

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Every partial recursive function is computed, in the accept-iff-defined sense on unary inputs, by a single-tape Turing machine.

Proof strategy

The source compiles the function, presented through mathlib's Nat.Partrec′Nat.Partrec', to a counter-machine program (Sim/Compile.leanSim/Compile.lean), and the program to a tape machine that walks over a tape of cells holding the counters (Sim/Simulate.leanSim/Simulate.lean); PCP.Sim.existstapemachinePCP.Sim.exists_tape_machine assembles the two. The concept's machine is the source's machine transported by ofSrcofSrc, and acceptance is transported by acceptsiffaccepts_iff.

Attribution

Lean development by Aristotle (RequestProject/Sim/RequestProject/Sim/); the statement is the Turing-completeness of Sipser's machines in the form the reduction needs.