Lax Lean Archive

Program execution

Lax213208.Programs · concepts/Lax213208/Programs.lean · lax-213208

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

    We use the archive's word-RAM programs. An output is returned if it is produced at every sufficiently large word width. This is an execution relation, not a computability claim or a running-time bound.

    A resource bound TT guarantees that input words and length fit in TT bits, and that the same output is produced within TT instructions at every width at least TT. Lax62's compilation theorems establish the underlying ComputesInTimeComputesInTime judgment from high-level program specifications.

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

    Lean source view on GitHub

    1import Lax808846.RamComputes
    2import Lax759944.RamPolytime
    3
    4/-!
    5---
    6title: Program execution
    7type: definition
    8---
    9We use the archive's word-RAM programs. An output is returned if it is
    10produced at every sufficiently large word width. This is an execution
    11relation, not a computability claim or a running-time bound.
    12
    13A resource bound TT guarantees that input words and length fit in TT bits,
    14and that the same output is produced within TT instructions at every
    15width at least TT. Lax62's compilation theorems establish the underlying
    16`ComputesInTime` judgment from high-level program specifications.
    17-/
    18
    19namespace Lax213208.Programs
    20
    21open Lax808846.Ram Lax808846.RamComputes Lax759944.RamPolytime
    22
    23abbrev Program := Lax808846.Ram.Program
    24
    25def Returns (alg : Program) (input output : List ℕ) : Prop :=
    26 ∃ width : ℕ, ∀ w ≥ width, ∃ steps, RunsTo w alg input output steps
    27
    28def RunsWithin (alg : Program) (input output : List ℕ) (bound : ℕ) : Prop :=
    29 FitsInWords bound (input.length :: input) ∧
    30 ∀ w ≥ bound, ComputesInTime w alg {input} (fun _ => output) (fun _ => bound)
    31
    32end Lax213208.Programs
    33
    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…