Lax Lean Archive

Finite-stack and elementary single-tape definitions of P

Lax434930.MachineModels · concepts/Lax434930/MachineModels.lean · lax-434930

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.

    Natural Language Statement

    Definition

    The finite-stack class requires every stack alphabet to be finite. The single-tape class uses a deterministic machine whose transitions each move the head one square or write one symbol. Its alphabet and control states are finite. The input is written in its original order, starting at the head, with blank tape elsewhere. The two input symbols are distinct and different from blank. A halted control state determines the Boolean answer; work tape need not be erased.

    Concept map
    2 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Lax434930.PolynomialTime
    2import Mathlib.Computability.TuringMachine.PostTuringMachine
    3
    4/-!
    5---
    6title: Finite-stack and elementary single-tape definitions of P
    7type: definition
    8---
    9The finite-stack class requires every stack alphabet to be finite. The
    10single-tape class uses a deterministic machine whose transitions each move
    11the head one square or write one symbol. Its alphabet and control states
    12are finite. The input is
    13written in its original order, starting at the head, with blank tape elsewhere.
    14The two input symbols are distinct and different from blank. A halted control
    15state determines the Boolean answer; work tape need not be erased.
    16-/
    17
    18namespace Lax434930.MachineModels
    19
    20open Turing PolynomialTime
    21
    22/-- Polynomial-time stack deciders with finite alphabets at every stack. -/
    23def FiniteStackP : Set Language :=
    24 {L | ∃ (f : Word → Bool)
    25 (M : TM2ComputableInPolyTime id Computability.encodeBool f),
    26 (∀ w, f w = true ↔ w ∈ L) ∧ ∀ k, Finite (M.tm.Γ k)}
    27
    28/-- A finite elementary single-tape machine, with ordinary binary input. -/
    29structure SingleTape where
    30 Γ : Type
    31 Q : Type
    32 [alphabet : Fintype Γ]
    33 [control : Fintype Q]
    34 [blank : Inhabited Γ]
    35 [initial : Inhabited Q]
    36 input : Bool ↪ Γ
    37 input_ne_blank : ∀ b, input b ≠ default
    38 transition : TM0.Machine Γ Q
    39 accept : Q → Bool
    40
    41attribute [instance] SingleTape.alphabet SingleTape.control SingleTape.blank SingleTape.initial
    42
    43/-- The standard single-tape formulation: one machine and one polynomial,
    44halting on every input, with acceptance exactly matching membership. -/
    45def SingleTapeP : Set Language :=
    46 {L | ∃ (M : SingleTape) (p : Polynomial ℕ), ∀ w : Word,
    47 ∃ c : TM0.Cfg M.Γ M.Q,
    48 Nonempty (StateTransition.EvalsToInTime (TM0.step M.transition)
    49 (TM0.init (w.map M.input)) (some c) (p.eval w.length)) ∧
    50 TM0.step M.transition c = none ∧ (M.accept c.q = true ↔ w ∈ L)}
    51
    52end Lax434930.MachineModels
    53
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…