Detailed Description

Mathematical programming — optimum as a typed constant.

Copyright: 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

optimization__Description

This module hosts compile-time problem classes from mathematical programming: linear programming (:lp), later quadratic programming (:qp) and beyond. The umbrella claim: for problem instances whose structure can be named at the type level — objective, constraints, active sets — the optimum is reducible to a typed constant (Singleton of the witnessing vertex / point) by the compiler, without runtime iteration.

This realises the paper's thesis in a sharpened form: the feasible polytope is a set-as-predicate, its finite vertex set is enumerated structurally, and the objective's ordering collapses the candidate set to a singleton optimum. "Rules on Buckets are Set" specialised to convex programming.

Note: "Modellbildung ist die halbe Miete." (Modelling is half the battle.) — Operations-research folk wisdom.

Roadmap (work in progress)

#319 undergraduate graph theory: the semiring closure and the critical path over a DAG; still open are Dijkstra and Bellman-Ford on general graphs, spanning trees, flows and matchings.
#330 undergraduate algorithms and data structures: dynamic programming as an algebraic path problem; still open are optimal substructure and memoisation as concepts, and topological sort.