Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.penalty

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/penalty.clj1 definitions, 2 theorems

AHoF O-family Penalty Method: solve a constrained optimization problem by a sequence of UNCONSTRAINED problems whose objective adds a penalty proportional to the constraint violation, penalized f mu violation = f + mu * violation where mu is the penalty coefficient (increased across outer iterations). As mu grows, minimizers are driven toward feasibility; at a feasible point the penalty vanishes and the penalized objective equals the true objective. Proved native and axiom-free: the penalized-objective combination; a worked penalized value; and that at zero violation (a feasible point) the penalized objective equals the original objective -- reducing by reflexivity. The base objective and the constraint-violation measure are executable; what is proved is the penalized objective combination. Requires nnrat/add, nnrat/multiply (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.penalty` prints this classification.

penalty/penalized :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

penalty/penalized-example :
  → pagerank/update 2 3 1 = 5

penalty/feasible-equals-objective :
  → pagerank/update 2 3 0 = 2