Lax Lean Archive

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

Lax47.Machine

Polynomial-time computation on the Lax51 finite-Turing model

concepts/Lax47/Machine.lean · lax-47

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

    All algorithms in this submission compute total functions on finite words of natural numbers. Polynomial time is exactly Lax51'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.

    Lean source view on GitHub

    1import Lax51.TuringPolytime
    2
    3/-!
    4---
    5title: Polynomial-time computation on the Lax51 finite-Turing model
    6type: definition
    7---
    8All algorithms in this submission compute total functions on finite words of
    9natural numbers. Polynomial time is exactly Lax51'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 Lax47.Machine
    22
    23open Lax51.BinaryWordEncoding Lax51.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
    57/-- A decision problem over finite words. -/
    58abbrev Language := Set BitString
    59
    60/-- A polynomial-time verifier whose certificate binary size is polynomially bounded. -/
    61structure NPVerifier (language : Language) where
    62 program : PolytimeProgram
    63 certificateConstant : ℕ
    64 certificateExponent : ℕ
    65 certificateConstant_pos : 0 < certificateConstant
    66 correctness : ∀ input : BitString,
    67 input ∈ language ↔ ∃ certificate : BitString,
    68 bitSize certificate ≤ polynomialBound
    69 certificateConstant certificateExponent (bitSize input) ∧
    70 program.output (pairBits input certificate) = [1]
    71
    72/-- Membership in NPNP in the Lax51 finite-Turing model. -/
    73def InNP (language : Language) : Prop :=
    74 Nonempty (NPVerifier language)
    75
    76/-- A polynomial-time randomized decision program using polynomially many uniform bits. -/
    77structure BPPAlgorithm (language : Language) where
    78 program : PolytimeProgram
    79 randomnessConstant : ℕ
    80 randomnessExponent : ℕ
    81 randomnessConstant_pos : 0 < randomnessConstant
    82 correctness : ∀ input : BitString,
    83 let randomBitCount := polynomialBound
    84 randomnessConstant randomnessExponent (bitSize input)
    85 let seeds : Finset (RandomSeed randomBitCount) := Finset.univ
    86 let accepting := seeds.filter fun seed ↦
    87 program.output (pairBits input seed.bits) = [1]
    88 (input ∈ language → 2 * seeds.card ≤ 3 * accepting.card) ∧
    89 (input ∉ language → 3 * accepting.card ≤ seeds.card)
    90
    91/-- Membership in BPPBPP in the same finite-Turing model. -/
    92def InBPP (language : Language) : Prop :=
    93 Nonempty (BPPAlgorithm language)
    94
    95/-- The complexity-class inclusion appearing in the inapproximability theorem. -/
    96def NPSubsetBPP : Prop :=
    97 ∀ language : Language, InNP language → InBPP language
    98
    99end Lax47.Machine
    100

    Builds on

    Used by

    From Mathlib

    none

    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…