Lax Lean Archive

Algorithm inputs

Lax213208.AlgorithmInput · concepts/Lax213208/AlgorithmInput.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

    An ordinary algorithm receives the instance's structural arena. A scheme receives the arena of (k,x)(k,x), where the positive integer kk specifies accuracy ε=1/k\varepsilon=1/k. Only the integer is machine input.

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

    Lean source view on GitHub

    1import Lax213208.OptimizationProblem
    2import Lax560851.StructuralCombinators
    3
    4/-!
    5---
    6title: Algorithm inputs
    7type: definition
    8---
    9An ordinary algorithm receives the instance's structural arena.
    10A scheme receives the arena of (k,x)(k,x), where the positive integer kk
    11specifies accuracy ε=1/k\varepsilon=1/k. Only the integer is machine input.
    12-/
    13
    14namespace Lax213208.AlgorithmInput
    15
    16open OptimizationProblem
    17open Lax560851.WordArena Lax560851.StructuralCombinators
    18
    19variable {Instance Solution : Type*}
    20
    21def inputTape (problem : Problem Instance Solution)
    22 (precision : Option ℕ) (x : Instance) : List ℕ :=
    23 match precision with
    24 | none => inputWords problem x
    25 | some k => (encode (prod nat problem.input) (k, x)).toInput
    26
    27end Lax213208.AlgorithmInput
    28
    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…