Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Environment v4.30.0. The archive's epoch is v4.33.0; only submissions in v4.30.0 can cite this work.

Time and word-capacity bounds on the word-RAM

Lax58.RamComplexity · concepts/Lax58/RamComplexity.lean · lax-58

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. 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 Lax13.RamComputes
    2import Lax58.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. No computability or growth restriction on either bound
    15is implicit: such restrictions belong in the theorem using this predicate.
    16
    17`RamComputableWithinUsing` is relative to explicitly supplied encodings; it
    18does not certify them. The `RamComputableWithin` frontend selects approved
    19encodings from the input and output types. Inputs use structural arenas;
    20natural and Boolean outputs use one word, and structured outputs use arenas.
    21-/
    22
    23namespace Lax58.RamComplexity
    24
    25open Lax13.Ram Lax13.RamComputes
    26open Lax58.StructuralPresentation Lax58.WordArena
    27
    28universe u v
    29
    30/-- Input size and payload magnitude for a specified presentation. -/
    31def inputMagnitudeUsing {α : Type u} (input : Presentation α) (x : α) : Nat :=
    32 (input.toRaw x).nodes + (input.toRaw x).maxNat + 1
    33
    34/-- A natural-number result occupies one output word. -/
    35def natOutput (n : Nat) : List Nat := [n]
    36
    37/-- A Boolean result occupies one output word: false is zero, true is one. -/
    38def boolOutput (b : Bool) : List Nat := [if b then 1 else 0]
    39
    40/-- A structured result uses the same root-plus-arena convention as input. -/
    41def arenaOutput {α : Type u} (raw : α → Raw) (x : α) : List Nat :=
    42 (encodeRaw (raw x)).toInput
    43
    44/-- One program for all inputs and all sufficient word widths, with explicit
    45encodings and exact instruction and word-capacity bounds. -/
    46def RamComputableWithinUsing {α : Type u} {β : Type v}
    47 (input : Presentation α) (output : β → List Nat)
    48 (f : α → β) (timeBound wordBound : α → Nat) : Prop :=
    49 ∃ program : Program,
    50 ∀ (x : α) (w : Nat),
    51 (input.toRaw x).PayloadsFitInWord w →
    52 3 * (input.toRaw x).nodes ≤ 2 ^ w →
    53 wordBound x ≤ 2 ^ w →
    54 ComputesInTime w program {(encode input x).toInput}
    55 (fun _ => output (f x)) (fun _ => timeBound x)
    56
    57end Lax58.RamComplexity
    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…