Lax Lean Archive

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

Lax554803.MachineModels

Finite-stack and elementary single-tape definitions of P

concepts/Lax554803/MachineModels.lean · lax-554803

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

    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.

    Lean source view on GitHub

    1import Lax554803.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 Lax554803.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 Lax554803.MachineModels
    53

    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…