Lax Lean Archive

L-reductions

Lax213208.LReduction · concepts/Lax213208/LReduction.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 L-reduction consists of polynomial-time instance and solution maps and positive constants a,ba,b. It maps valid instances and feasible solutions to valid instances and feasible solutions, and satisfies OPTB(f(x))≤a OPTA(x)\mathrm{OPT}_B(f(x))\le a\,\mathrm{OPT}_A(x) and ∣OPTA(x)−vA(g(x,y))∣≤b ∣OPTB(f(x))−vB(y)∣|\mathrm{OPT}_A(x)-v_A(g(x,y))| \le b\,|\mathrm{OPT}_B(f(x))-v_B(y)|.

    Optima are required to be attained. The solution map receives both xx and yy; its time is measured in their combined encoded size. Their word lists are paired by prefixing the length of the first list.

    Concept map
    11 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax213208.Approximation
    2import Lax213208.PolynomialComputation
    3
    4/-!
    5---
    6title: L-reductions
    7type: definition
    8---
    9An L-reduction consists of polynomial-time instance and solution maps and
    10positive constants a,ba,b. It maps valid instances and feasible solutions
    11to valid instances and feasible solutions, and satisfies
    12OPTB(f(x))≤a OPTA(x)\mathrm{OPT}_B(f(x))\le a\,\mathrm{OPT}_A(x) and
    13∣OPTA(x)−vA(g(x,y))∣≤b ∣OPTB(f(x))−vB(y)∣|\mathrm{OPT}_A(x)-v_A(g(x,y))| \le b\,|\mathrm{OPT}_B(f(x))-v_B(y)|
    14.
    15
    16Optima are required to be attained. The solution map receives both xx
    17and yy; its time is measured in their combined encoded size. Their word
    18lists are paired by prefixing the length of the first list.
    19-/
    20
    21namespace Lax213208.LReduction
    22
    23open OptimizationProblem Approximation PolynomialComputation
    24
    25variable {SourceInstance SourceSolution TargetInstance TargetSolution : Type*}
    26
    27def solutionMapInput (source : Problem SourceInstance SourceSolution)
    28 (target : Problem TargetInstance TargetSolution)
    29 (xy : SourceInstance × TargetSolution) : List ℕ :=
    30 let first := inputWords source xy.1
    31 first.length :: (first ++ target.output xy.2)
    32
    33structure LReduction (source : Problem SourceInstance SourceSolution)
    34 (target : Problem TargetInstance TargetSolution)
    35 (sourceInputs : Set SourceInstance) (targetInputs : Set TargetInstance) where
    36 instanceMap : SourceInstance → TargetInstance
    37 solutionMap : SourceInstance → TargetSolution → SourceSolution
    38 optimumFactor : ℝ
    39 errorFactor : ℝ
    40 optimumFactor_pos : 0 < optimumFactor
    41 errorFactor_pos : 0 < errorFactor
    42 instanceMap_polytime :
    43 PolynomialTimeComputable (inputWords source) (inputWords target) instanceMap sourceInputs
    44 solutionMap_polytime :
    45 PolynomialTimeComputable (solutionMapInput source target) source.output
    46 (fun xy => solutionMap xy.1 xy.2)
    47 {xy | xy.1 ∈ sourceInputs ∧ target.feasible (instanceMap xy.1) xy.2}
    48 maps_instances : ∀ x ∈ sourceInputs, instanceMap x ∈ targetInputs
    49 maps_solutions : ∀ x ∈ sourceInputs, ∀ y, target.feasible (instanceMap x) y →
    50 source.feasible x (solutionMap x y)
    51 bounds : ∀ x ∈ sourceInputs, ∃ sourceOpt targetOpt : ℝ,
    52 IsOptimalValue source x sourceOpt ∧
    53 IsOptimalValue target (instanceMap x) targetOpt ∧
    54 targetOpt ≤ optimumFactor * sourceOpt ∧
    55 ∀ y, target.feasible (instanceMap x) y →
    56 |sourceOpt - source.value x (solutionMap x y)| ≤
    57 errorFactor * |targetOpt - target.value (instanceMap x) y|
    58
    59end Lax213208.LReduction
    60
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…