Documentation

Provenance.Algorithms.SumDP

Correctness of SUM enumeration via dynamic programming #

This file formalises 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 #

source
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
Instances For
    source
    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.
    Instances For

      Correctness lemmas #

      source
      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 characterisation 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').

      source
      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.