Lax Lean Archive

Time and word-capacity bounds on the word-RAM

Lax560851.RamComplexity · concepts/Lax560851/RamComplexity.lean · lax-560851

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

    One fixed program computes a mathematical function within explicit time and word-capacity bounds. It works at every word width satisfying the input-fit conditions and the supplied capacity threshold. The threshold is a number of representable values, not a number of bits. Output production is included in the instruction count, including a fetched final halthalt or exhausted readread. The arena is supplied on Lax808846's immutable input array and sequential tape; writable memory starts at zero. No computability or growth restriction on either bound is implicit: such restrictions belong in the theorem using this predicate.

    RamComputableWithinUsingRamComputableWithinUsing is relative to explicitly supplied encodings; it does not certify them. The RamComputableWithinRamComputableWithin frontend selects approved encodings from the input and output types. Inputs use structural arenas; natural and Boolean outputs use one word, and structured outputs use arenas.

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

    Lean source view on GitHub

    1import Lax808846.RamComputes
    2import Lax560851.WordArena
    3
    4/-!
    5---
    6title: Time and word-capacity bounds on the word-RAM
    7type: definition
    8---
    9
    10One fixed program computes a mathematical function within explicit time and
    11word-capacity bounds. It works at every word width satisfying the input-fit
    12conditions and the supplied capacity threshold. The threshold is a number of
    13representable values, not a number of bits. Output production is included in
    14the instruction count, including a fetched final `halt` or exhausted `read`.
    15The arena is supplied on Lax808846's immutable input array and sequential
    16tape; writable memory starts at zero. No computability or growth restriction
    17on either bound is implicit: such restrictions belong in the theorem using this predicate.
    18
    19`RamComputableWithinUsing` is relative to explicitly supplied encodings; it
    20does not certify them. The `RamComputableWithin` frontend selects approved
    21encodings from the input and output types. Inputs use structural arenas;
    22natural and Boolean outputs use one word, and structured outputs use arenas.
    23-/
    24
    25namespace Lax560851.RamComplexity
    26
    27open Lax808846.Ram Lax808846.RamComputes
    28open Lax560851.StructuralPresentation Lax560851.WordArena
    29
    30universe u v
    31
    32/-- Input size and payload magnitude for a specified presentation. -/
    33def inputMagnitudeUsing {α : Type u} (input : Presentation α) (x : α) : Nat :=
    34 (input.toRaw x).nodes + (input.toRaw x).maxNat + 1
    35
    36/-- A natural-number result occupies one output word. -/
    37def natOutput (n : Nat) : List Nat := [n]
    38
    39/-- A Boolean result occupies one output word: false is zero, true is one. -/
    40def boolOutput (b : Bool) : List Nat := [if b then 1 else 0]
    41
    42/-- A structured result uses the same root-plus-arena convention as input. -/
    43def arenaOutput {α : Type u} (raw : α → Raw) (x : α) : List Nat :=
    44 (encodeRaw (raw x)).toInput
    45
    46/-- One program for all inputs and all sufficient word widths, with explicit
    47encodings and exact instruction and word-capacity bounds. -/
    48def RamComputableWithinUsing {α : Type u} {β : Type v}
    49 (input : Presentation α) (output : β → List Nat)
    50 (f : α → β) (timeBound wordBound : α → Nat) : Prop :=
    51 ∃ program : Program,
    52 ∀ (x : α) (w : Nat),
    53 (input.toRaw x).PayloadsFitInWord w →
    54 3 * (input.toRaw x).nodes ≤ 2 ^ w →
    55 wordBound x ≤ 2 ^ w →
    56 ComputesInTime w program {(encode input x).toInput}
    57 (fun _ => output (f x)) (fun _ => timeBound x)
    58
    59end Lax560851.RamComplexity
    60
    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…