Documentation

Provenance.Algorithms.SumDP

Correctness of Algorithm 1: SUM enumeration via dynamic programming #

This file formalises Algorithm 1 of the HAVING / ProvSQL paper. 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 paper presents the algorithm as an imperative subset-sum dynamic program with an in-place dp[j] array, bounded by 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., the paper's dp[j] after iteration N), defined by direct recursion on occs. The six op-cases of the algorithm 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 α → ℕ; the annotation α_i of the paper is 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 dp[j] after the outer loop of Algorithm 1: 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) of Algorithm 1. The six operator-cases of the paper (and the four early-return cases) 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 Algorithm 1 (thm:sumdp-correct of the paper). 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.