Lax Lean Archive

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

Lax251941.TuringCompleteness

Every partial recursive function is computed by a Turing machine

concepts/Lax251941/TuringCompleteness.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

    For every partial recursive function f:N⇀Nf : \mathbb{N} \rightharpoonup \mathbb{N} there is a single-tape Turing machine which, on the unary encoding of nn, reaches its accept state exactly when f(n)f(n) is defined. This is the Turing-completeness of the string-rewriting machines of TuringMachinesTuringMachines, in the form in which it links Sipser's two sections: the diagonalisation of Section 4.2 is carried out for partial recursive programs, the reduction of Section 5.2 for tape machines, and this theorem is what makes the acceptance problem of the latter as hard as that of the former.

    Lean source view on GitHub

    1import Mathlib.Computability.Partrec
    2import Lax251941.TuringMachines
    3
    4/-!
    5---
    6title: Every partial recursive function is computed by a Turing machine
    7type: theorem
    8---
    9For every partial recursive function f:N⇀Nf : \mathbb{N} \rightharpoonup \mathbb{N}
    10there is a single-tape Turing machine which, on the unary encoding of nn,
    11reaches its accept state exactly when f(n)f(n) is defined. This is the
    12Turing-completeness of the string-rewriting machines of `TuringMachines`, in
    13the form in which it links Sipser's two sections: the diagonalisation of
    14Section 4.2 is carried out for partial recursive programs, the reduction of
    15Section 5.2 for tape machines, and this theorem is what makes the acceptance
    16problem of the latter as hard as that of the former.
    17
    18# Formalization notes
    19
    20The unary encoding of `n` is the word `mk :: replicate n c` for two tape symbols
    21`mk` (a marker) and `c` (a counter cell) chosen by the theorem together with
    22the machine. `Partrec` is mathlib's class of partial recursive functions
    23`ℕ →. ℕ`. The proof compiles the function to a counter-machine program and the
    24program to a tape machine; the compiled machine is deterministic, although the
    25model allows nondeterminism.
    26-/
    27
    28namespace Lax251941.TuringCompleteness
    29
    30open Lax251941.TuringMachines
    31
    32/-- For every partial recursive `f` there is a tape machine, with a marker symbol
    33and a counter symbol, that accepts the unary encoding of `n` exactly when `f n` is
    34defined. -/
    35axiom exists_tm_accepts_iff_dom (f : ℕ →. ℕ) (hf : Partrec f) :
    36 ∃ (M : TM) (mk c : ℕ), ∀ n : ℕ, M.Accepts (mk :: List.replicate n c) ↔ (f n).Dom
    37
    38end Lax251941.TuringCompleteness
    39
    Show Proof

    Formalization notes

    The unary encoding of nn is the word mk::replicatencmk :: replicate n c for two tape symbols mkmk (a marker) and cc (a counter cell) chosen by the theorem together with the machine. PartrecPartrec is mathlib's class of partial recursive functions N→.Nℕ →. ℕ. The proof compiles the function to a counter-machine program and the program to a tape machine; the compiled machine is deterministic, although the model allows nondeterminism.

    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…