Lax Lean Archive

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

Lax251941.TapeAcceptanceUndecidable

The acceptance problem for Turing machines is undecidable

concepts/Lax251941/TapeAcceptanceUndecidable.lean · lax-251941

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    No algorithm decides, given a single-tape Turing machine MM and an input word ww, whether MM accepts ww. This is Sipser's Theorem 4.11 for the tape machines of Section 5.2: a decision procedure for their acceptance problem would, through the Turing-completeness of the tape machines (TuringCompletenessTuringCompleteness), decide the acceptance problem ATMA_{TM} of AcceptanceAcceptance, which the diagonalisation argument rules out. One simulation suffices, since a decision procedure is uniform in the machine: the machine simulating a fixed universal function is held fixed and only its input varies.

    Lean source view on GitHub

    1import Mathlib.Computability.Halting
    2import Lax251941.TuringMachines
    3
    4/-!
    5---
    6title: The acceptance problem for Turing machines is undecidable
    7type: theorem
    8---
    9No algorithm decides, given a single-tape Turing machine MM and an input word
    10ww, whether MM accepts ww. This is Sipser's Theorem 4.11 for the tape
    11machines of Section 5.2: a decision procedure for their acceptance problem
    12would, through the Turing-completeness of the tape machines
    13(`TuringCompleteness`), decide the acceptance problem ATMA_{TM} of
    14`Acceptance`, which the diagonalisation argument rules out. One simulation
    15suffices, since a decision procedure is uniform in the machine: the machine
    16simulating a fixed universal function is held fixed and only its input varies.
    17
    18# Formalization notes
    19
    20Decidability of a problem on pairs `(M, w)` is mathlib's `ComputablePred` on the
    21type `TM × List ℕ`, with machines encoded by their tables (the `Primcodable`
    22instance of `TuringMachines`).
    23-/
    24
    25namespace Lax251941.TapeAcceptanceUndecidable
    26
    27open Lax251941.TuringMachines
    28
    29/-- The acceptance problem for single-tape Turing machines is undecidable. -/
    30axiom not_computablePred_accepts :
    31 ¬ ComputablePred fun p : TM × List ℕ => p.1.Accepts p.2
    32
    33end Lax251941.TapeAcceptanceUndecidable
    34
    Show Proof

    Formalization notes

    Decidability of a problem on pairs (M,w)(M, w) is mathlib's ComputablePredComputablePred on the type TM×ListNTM × List ℕ, with machines encoded by their tables (the PrimcodablePrimcodable instance of TuringMachinesTuringMachines).

    Builds on

    Used by

    none

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…