Correctness of SUM enumeration via dynamic programming

This file formalizes a subset-sum enumeration algorithm. The algorithm enumerates the non-empty subsets W of a finite set of occurrences U whose weighted sum ∑_{u ∈ W} t u satisfies (∑ t) op C for a fixed comparison operator op and constant C : ℕ. The main result sumDP_correct shows that the output coincides with that set in the sense of membership.

The standard imperative presentation uses an in-place dp[j] array bounded by some J chosen per operator, with early returns for impossible operator/constant combinations. We use the mathematically equivalent functional formulation: sumExact occs t j is the list of subsets of occs.toFinset with weighted sum exactly j (i.e., dp[j] after iteration N), defined by direct recursion on occs. The six op-cases and all four early-return cases collapse into a single flatMap over satisfying sums in {0, …, T}, where T = occs.toFinset.sum t. Impossible sums simply contribute empty enumerations.

The aggregate term t enters as α → ℕ; an annotation α_i would be part of the occurrence type and does not enter the sum.

Definitions

def SumDP.sumExact {α : Type u_1} [DecidableEq α] : List α → (α → ℕ) → ℕ → List (Finset α)

sumExact occs t j: enumerate the subsets of occs.toFinset whose weighted sum under t is exactly j. Mirrors the dynamic-programming table dp[j] after the outer loop: every subset either omits the head u (left recursion) or includes it (right recursion, requires t u ≤ j).

Equations

• SumDP.sumExact [] x✝ 0 = [∅]
• SumDP.sumExact [] x✝ n.succ = []
• SumDP.sumExact (u :: rest) x✝¹ x✝ = SumDP.sumExact rest x✝¹ x✝ ++ if x✝¹ u ≤ x✝ then List.map (insert u) (SumDP.sumExact rest x✝¹ (x✝ - x✝¹ u)) else []

def SumDP.sumDP {α : Type u_1} [DecidableEq α] (occs : List α) (t : α → ℕ) (C : ℕ) (op : CompOp) : List (Finset α)

SumDP(U, t, C, op): top-level routine. The six operator-cases (and the four early-return cases of a more imperative presentation) collapse into a single flatMap over satisfying sums in {0, …, T}, where T is the total weight occs.toFinset.sum t.

Equations

• One or more equations did not get rendered due to their size.

Correctness lemmas

theorem SumDP.sumExact_mem {α : Type u_1} [DecidableEq α] (occs : List α) : occs.Nodup → ∀ (t : α → ℕ) (j : ℕ) (S : Finset α), S ∈ sumExact occs t j ↔ S ⊆ occs.toFinset ∧ S.sum t = j

Membership characterization of sumExact. Under occs.Nodup, the output enumerates exactly the subsets of occs.toFinset with weighted sum equal to j. The Nodup hypothesis is used in the inductive step to guarantee that the head u does not appear later in rest, so that insert u S' with S' ⊆ rest.toFinset genuinely adds t u to the sum (rather than collapsing to S').

theorem SumDP.sumExact_nodup {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (t : α → ℕ) (j : ℕ) : (sumExact occs t j).Nodup

The enumeration sumExact contains no duplicate subset. Nodup of occs guarantees that the head u is absent from the subsets produced by the recursive calls, so the insert u copies are pairwise distinct and disjoint from the u-free part of the output.

theorem SumDP.sumDP_nodup {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (t : α → ℕ) (C : ℕ) (op : CompOp) : (sumDP occs t C op).Nodup

The top-level enumeration sumDP contains no duplicate subset: within one bucket j by sumExact_nodup, and across buckets because a subset in bucket j has weighted sum exactly j. This is not cosmetic: the provenance attached to the enumeration is the ⊕-sum of the world annotations over the returned list, and in a non-idempotent m-semiring a duplicated world would change the value.

theorem SumDP.sumDP_correct {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (t : α → ℕ) (C : ℕ) (op : CompOp) (S : Finset α) : S ∈ sumDP occs t C op ↔ S ⊆ occs.toFinset ∧ S ≠ ∅ ∧ op.eval (S.sum t) C

Correctness of sumDP. For a list occs of distinct occurrences, a weight function t, a constant C : ℕ, and a comparison operator op, the list sumDP occs t C op enumerates exactly the non-empty subsets S ⊆ occs.toFinset whose weighted sum satisfies op.eval (S.sum t) C.

Soundness of the implementation optimizations

The imperative implementation of the algorithm bounds its dp table by an operator-specific J = min(C, T) for the operators =, ≤, <, prunes dp[j] cells beyond the running prefix sum, and short-circuits comparisons that no achievable sum can satisfy. Each optimization is proved as a list equality with the unoptimized enumeration: the optimized enumerations return the same worlds, so the downstream ⊕-sum of world annotations is unchanged.

theorem SumDP.sumDP_eq_bounded {α : Type u_1} [DecidableEq α] (occs : List α) (t : α → ℕ) (C : ℕ) {op : CompOp} (hop : op = CompOp.eq ∨ op = CompOp.le ∨ op = CompOp.lt) : sumDP occs t C op = List.flatMap (fun (j : ℕ) => List.filter (fun (S : Finset α) => decide (S ≠ ∅)) (sumExact occs t j)) (List.filter (fun (j : ℕ) => decide (op.eval j C)) (List.range (min C (occs.toFinset.sum t) + 1)))

Operator-specific bound on the dp table. For op ∈ {=, ≤, <}, no sum above C satisfies the comparison, so the enumeration may range over {0, …, min(C, T)} instead of {0, …, T} and return the same list.

theorem SumDP.sumExact_eq_nil_of_lt_sum {α : Type u_1} [DecidableEq α] (occs : List α) (t : α → ℕ) {j : ℕ} : (List.map t occs).sum < j → sumExact occs t j = []

Reachability pruning. Above the total weight of the occurrence list (in the imperative formulation: above the running prefix sum at each step of the recursion), the dp cells are empty: sumExact occs t j = [] as soon as j exceeds (occs.map t).sum. No Nodup hypothesis is needed.

theorem SumDP.sumExact_eq_nil_of_lt_sum' {α : Type u_1} [DecidableEq α] (occs : List α) (hnodup : occs.Nodup) (t : α → ℕ) {j : ℕ} (h : occs.toFinset.sum t < j) : sumExact occs t j = []

Under Nodup, the reachability bound can be read on the total weight T = ∑_{u ∈ occs} t u of the distinct occurrences.

theorem SumDP.sumDP_eq_nil_of_unsat {α : Type u_1} [DecidableEq α] (occs : List α) (t : α → ℕ) (C : ℕ) (op : CompOp) (h : ∀ j ≤ occs.toFinset.sum t, ¬op.eval j C) : sumDP occs t C op = []

Range check, unsatisfiable side. If no achievable sum satisfies the comparison, the enumeration is empty (and the associated provenance is 𝟘, an empty ⊕-sum).

Home · Documentation · Publications · Contributors · Source · Cite