Reduction of optimization problems #
We define the notion of reduction. It is a reflexive and transitive relation and it induces a backward map between solutions. The idea is that solving the reduced problem is "as hard" as solving the original problem. An equivalence gives a reduction.
References #
- [Pap93] C. Papadimitriou, Computational Complexity
TODO #
- Build reductions from equivalences automatically in meta.
structure
Minimization.Reduction
{D : Type}
{E : Type}
{R : Type}
[Preorder R]
(p : Minimization D R)
(q : Minimization E R)
:
We read Reduction p q as p reduces to q [Pap93,10.1].
- psi : E → D
- psi_optimality : ∀ (x : E), q.optimal x → p.optimal (self.psi x)
Instances For
theorem
Minimization.Reduction.psi_optimality
{D : Type}
{E : Type}
{R : Type}
[Preorder R]
{p : Minimization D R}
{q : Minimization E R}
(self : p.Reduction q)
(x : E)
:
q.optimal x → p.optimal (self.psi x)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Minimization.Reduction.refl
{D : Type}
{R : Type}
[Preorder R]
{p : Minimization D R}
:
p.Reduction p
Equations
- Minimization.Reduction.refl = { psi := id, psi_optimality := ⋯ }
Instances For
def
Minimization.Reduction.trans
{D : Type}
{E : Type}
{F : Type}
{R : Type}
[Preorder R]
{p : Minimization D R}
{q : Minimization E R}
{r : Minimization F R}
(R₁ : p.Reduction q)
(R₂ : q.Reduction r)
:
p.Reduction r
Instances For
instance
Minimization.Reduction.instTrans
{D : Type}
{E : Type}
{F : Type}
{R : Type}
[Preorder R]
:
Trans Minimization.Reduction Minimization.Reduction Minimization.Reduction
Equations
- Minimization.Reduction.instTrans = { trans := fun {a : Minimization D R} {b : Minimization E R} {c : Minimization F R} => Minimization.Reduction.trans }
def
Minimization.Reduction.toBwd
{D : Type}
{E : Type}
{R : Type}
[Preorder R✝]
{p : Minimization D R✝}
{q : Minimization E R✝}
(R : p.Reduction q)
:
q.Solution → p.Solution
Equations
- R.toBwd sol = { point := R.psi sol.point, isOptimal := ⋯ }
Instances For
def
Minimization.Reduction.ofEquivalence
{D : Type}
{E : Type}
{R : Type}
[Preorder R]
{p : Minimization D R}
{q : Minimization E✝ R}
(E : p.Equivalence q)
:
p.Reduction q
Equations
- Minimization.Reduction.ofEquivalence E = { psi := E.psi, psi_optimality := ⋯ }
Instances For
def
Minimization.Reduction.map_objFun_of_order_reflecting
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{g : R → R}
{cs : D → Prop}
(h : ∀ {r s : D}, cs r → cs s → g (f r) ≤ g (f s) → f r ≤ f s)
:
{ objFun := f, constraints := cs }.Reduction { objFun := fun (x : D) => g (f x), constraints := cs }
Weaker version of Equivalence.map_objFun. For a reduction we only need the map to be
order-reflecting on the image of the objective function. Note that for an equivalence we also need
it to be order-preserving (order-reflecting + order-preserving = order embedding).
Equations
- Minimization.Reduction.map_objFun_of_order_reflecting h = { psi := id, psi_optimality := ⋯ }
Instances For
def
Minimization.Reduction.map_objFun
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{g : R → R}
{cs : D → Prop}
(h : ∀ {r s : D}, cs r → cs s → (g (f r) ≤ g (f s) ↔ f r ≤ f s))
:
{ objFun := f, constraints := cs }.Reduction { objFun := fun (x : D) => g (f x), constraints := cs }
See Equivalence.map_objFun.
Equations
Instances For
noncomputable def
Minimization.Reduction.map_objFun_log
{D : Type}
{cs : D → Prop}
{f : D → ℝ}
(h : ∀ (x : D), cs x → f x > 0)
:
{ objFun := f, constraints := cs }.Reduction { objFun := fun (x : D) => (f x).log, constraints := cs }
See Equivalence.map_objFun_log.
Equations
Instances For
noncomputable def
Minimization.Reduction.map_objFun_sq
{D : Type}
{cs : D → Prop}
{f : D → ℝ}
(h : ∀ (x : D), cs x → f x ≥ 0)
:
{ objFun := f, constraints := cs }.Reduction { objFun := fun (x : D) => f x ^ 2, constraints := cs }
See Equivalence.map_objFun_sq.
Equations
Instances For
def
Minimization.Reduction.map_domain
{D : Type}
{E : Type}
{R : Type}
[Preorder R]
{f : D → R}
{cs : D → Prop}
{fwd : D → E}
{bwd : E → D}
(h : ∀ (x : D), cs x → bwd (fwd x) = x)
:
{ objFun := f, constraints := cs }.Reduction
{ objFun := fun (x : E) => f (bwd x), constraints := fun (x : E) => cs (bwd x) }
See Equivalence.map_domain.
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_1_last
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c1' : D → Prop}
(hrw : ∀ (x : D), c1 x ↔ c1' x)
:
{ objFun := f, constraints := fun (x : D) => c1 x }.Reduction { objFun := f, constraints := fun (x : D) => c1' x }
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_5
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c5' : D → Prop}
{cs : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → cs x → (c5 x ↔ c5' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_6
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c6' : D → Prop}
{cs : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → cs x → (c6 x ↔ c6' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_6_last
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c6' : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → (c6 x ↔ c6' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_7
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c7' : D → Prop}
{cs : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → cs x → (c7 x ↔ c7' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_7_last
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c7' : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → (c7 x ↔ c7' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_8
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c8 : D → Prop}
{c8' : D → Prop}
{cs : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → cs x → (c8 x ↔ c8' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_8_last
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c8 : D → Prop}
{c8' : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → (c8 x ↔ c8' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_9
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c8 : D → Prop}
{c9 : D → Prop}
{c9' : D → Prop}
{cs : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → c8 x → cs x → (c9 x ↔ c9' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_9_last
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c8 : D → Prop}
{c9 : D → Prop}
{c9' : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → c8 x → (c9 x ↔ c9' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_10
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c8 : D → Prop}
{c9 : D → Prop}
{c10 : D → Prop}
{c10' : D → Prop}
{cs : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → c8 x → c9 x → cs x → (c10 x ↔ c10' x))
:
Equations
Instances For
def
Minimization.Reduction.rewrite_constraint_10_last
{D : Type}
{R : Type}
[Preorder R]
{f : D → R}
{c1 : D → Prop}
{c2 : D → Prop}
{c3 : D → Prop}
{c4 : D → Prop}
{c5 : D → Prop}
{c6 : D → Prop}
{c7 : D → Prop}
{c8 : D → Prop}
{c9 : D → Prop}
{c10 : D → Prop}
{c10' : D → Prop}
(hrw : ∀ (x : D), c1 x → c2 x → c3 x → c4 x → c5 x → c6 x → c7 x → c8 x → c9 x → (c10 x ↔ c10' x))
:
Equations
Instances For
def
Minimization.Equivalence.ofReductions
{D : Type}
{E : Type}
{R : Type}
[Preorder R]
(p : Minimization D R)
(q : Minimization E R)
(R₁ : p.Reduction q)
(R₂ : q.Reduction p)
:
p.Equivalence q
Equations
- Minimization.Equivalence.ofReductions p q R₁ R₂ = { phi := R₂.psi, psi := R₁.psi, phi_optimality := ⋯, psi_optimality := ⋯ }