Lax Lean Archive

Polynomial-time computation on the Lax759944 finite-Turing model

Lax614640.Machine · concepts/Lax614640/Machine.lean · lax-614640

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

    All algorithms in this submission compute total functions on finite words of natural numbers. Polynomial time is exactly Lax759944's predicate: a fixed finite multi-stack Turing machine transforms the canonical binary encoding of the input word into the canonical binary encoding of its output within a polynomial number of transitions.

    In particular, a program's semantic function is tied to an actual finite Turing machine by TuringPolytimeTuringPolytime. Randomized algorithms receive a finite list of independent uniform bits, represented by the words 00 and 11.

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

    Lean source view on GitHub

    1import Lax759944.TuringPolytime
    2
    3/-!
    4---
    5title: Polynomial-time computation on the Lax759944 finite-Turing model
    6type: definition
    7---
    8All algorithms in this submission compute total functions on finite words of
    9natural numbers. Polynomial time is exactly Lax759944's predicate: a fixed
    10finite multi-stack Turing machine transforms the canonical binary encoding of
    11the input word into the canonical binary encoding of its output within a
    12polynomial number of transitions.
    13
    14In particular, a program's semantic function is tied to an actual finite
    15Turing machine by TuringPolytimeTuringPolytime. Randomized algorithms receive a finite
    16list of independent uniform bits, represented by the words 00 and 11.
    17-/
    18
    19set_option autoImplicit false
    20
    21namespace Lax614640.Machine
    22
    23open Lax759944.BinaryWordEncoding Lax759944.TuringPolytime
    24
    25/-- A finite machine word. Boolean data use the entries 00 and 11. -/
    26abbrev BitString := List ℕ
    27
    28/-- The convenient monomial bound c(n+1)kc(n+1)^k. -/
    29def polynomialBound (c k n : ℕ) : ℕ :=
    30 c * (n + 1) ^ k
    31
    32/-- A total word function computed in polynomial time by a finite Turing machine. -/
    33structure PolytimeProgram where
    34 function : BitString → BitString
    35 polytime : TuringPolytime function
    36
    37/-- The semantic output certified by the program's finite Turing machine. -/
    38def PolytimeProgram.output (program : PolytimeProgram)
    39 (input : BitString) : BitString :=
    40 program.function input
    41
    42/-- A length-prefixed pairing of two finite words. -/
    43def pairBits (left right : BitString) : BitString :=
    44 left.length :: left ++ right
    45
    46/-- A uniformly random string of exactly rr bits. -/
    47abbrev RandomSeed (r : ℕ) := Fin r → Bool
    48
    49/-- Encode one Boolean as a natural-number word. -/
    50def bitWord (bit : Bool) : ℕ :=
    51 if bit then 1 else 0
    52
    53/-- The word representation of a fixed-length random seed. -/
    54def RandomSeed.bits {r : ℕ} (seed : RandomSeed r) : BitString :=
    55 (List.ofFn seed).map bitWord
    56
    57end Lax614640.Machine
    58
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…