Lax Lean Archive

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

Lax489179.TuringMachine

Finite multitape Turing machines

concepts/Lax489179/TuringMachine.lean · lax-489179

definition

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

    Definition

    A machine has a fixed finite number of tapes, symbols and control states. Each transition reads the scanned symbols, writes one symbol per tape, and moves each head by at most one cell. Halting returns one Boolean. Tapes are indexed by integers. Initially all heads are at zero; tape zero contains the binary input in its original order and every other cell is blank. Blank, false and true are distinct symbols.

    A randomized transition may also inspect one fresh fair bit. A deterministic machine has the same transition for both values of that bit. One transition, including the transition returning an answer, costs one step. The finite transition table is chosen before the input. This elementary multitape model avoids any uncharged computation inside a transition and is used for the SAT hypotheses.

    Lean source view on GitHub

    1import Lax489179.Algorithms
    2import Mathlib.Data.Int.Basic
    3
    4/-!
    5---
    6title: Finite multitape Turing machines
    7type: definition
    8---
    9A machine has a fixed finite number of tapes, symbols and control states.
    10Each transition reads the scanned symbols, writes one symbol per tape,
    11and moves each head by at most one cell. Halting returns one Boolean.
    12Tapes are indexed by integers. Initially all heads are at zero; tape zero
    13contains the binary input in its original order and every other cell is
    14blank. Blank, false and true are distinct symbols.
    15
    16A randomized transition may also inspect one fresh fair bit. A
    17deterministic machine has the same transition for both values of that
    18bit. One transition, including the transition returning an answer,
    19costs one step. The finite transition table is chosen before the input.
    20This elementary multitape model avoids any uncharged computation inside
    21a transition and is used for the SAT hypotheses.
    22-/
    23
    24namespace Lax489179.TuringMachine
    25
    26inductive Move
    27 | left
    28 | stay
    29 | right
    30
    31def Move.offset : Move → ℤ
    32 | .left => -1
    33 | .stay => 0
    34 | .right => 1
    35
    36inductive Instruction (tapes symbols states : ℕ)
    37 | halt (answer : Bool)
    38 | next (state : Fin states) (write : Fin tapes → Fin symbols)
    39 (move : Fin tapes → Move)
    40
    41/-- The added constants ensure a nonempty control and tape set and
    42three distinct input/blank symbols. -/
    43structure Machine where
    44 tapes : ℕ
    45 symbols : ℕ
    46 states : ℕ
    47 transition : Fin (states + 1) → (Fin (tapes + 1) → Fin (symbols + 3)) →
    48 Bool → Instruction (tapes + 1) (symbols + 3) (states + 1)
    49
    50structure Config (M : Machine) where
    51 state : Fin (M.states + 1)
    52 head : Fin (M.tapes + 1) → ℤ
    53 tape : Fin (M.tapes + 1) → ℤ → Fin (M.symbols + 3)
    54 answer : Option Bool
    55
    56def init (M : Machine) (input : List Bool) : Config M where
    57 state := 0
    58 head := fun _ => 0
    59 tape := fun j z =>
    60 if j = 0 ∧ 0 ≤ z then
    61 match input[z.toNat]? with
    62 | none => 0
    63 | some false => 1
    64 | some true => 2
    65 else 0
    66 answer := none
    67
    68/-- A halted configuration is unchanged, allowing a run to be padded. -/
    69def step (M : Machine) (coin : Bool) (c : Config M) : Config M :=
    70 match c.answer with
    71 | some _ => c
    72 | none =>
    73 match M.transition c.state (fun j => c.tape j (c.head j)) coin with
    74 | .halt b => { c with answer := some b }
    75 | .next q write move =>
    76 { state := q
    77 head := fun j => c.head j + (move j).offset
    78 tape := fun j z => if z = c.head j then write j else c.tape j z
    79 answer := none }
    80
    81def run (M : Machine) : (t : ℕ) → (Fin t → Bool) → Config M → Config M
    82 | 0, _, c => c
    83 | t + 1, r, c => run M t (fun i => r i.succ) (step M (r 0) c)
    84
    85def Deterministic (M : Machine) : Prop :=
    86 ∀ q scanned, M.transition q scanned false = M.transition q scanned true
    87
    88def DecidesWithin (M : Machine) (input : List Bool) (answer : Prop) (t : ℕ) : Prop :=
    89 Algorithms.CorrectWithin t (fun r => (run M t r (init M input)).answer)
    90 (fun b => b = true ↔ answer)
    91
    92end Lax489179.TuringMachine
    93

    Builds on

    Used by

    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…