Kind-indexed general queries and their annotated semantics

The general (non-fused) HAVING semantics: aggregate values produced by a grouping operator γ^≼ are carried through further operators – projection, join, union, additional selections – as symbolic tokens (AggValue) in dedicated columns, and compared downstream, the possible worlds of such a comparison being those of the originating group.

Kind-indexed syntax

Queries are indexed by a column-kind vector κ : Fin n → ColKind (regular vs aggregate-token), so that the scope conditions are enforced statically and no theorem carries a well-formedness hypothesis:

• Gamma (the decomposed γ^≼) takes an all-regular input – no aggregation over aggregate values;
• Dedup and Diff exist only at all-regular kind vectors – no deduplication or difference over token columns (ProvSQL rejects these);
• projection columns are either regular terms over regular columns (ProjCol.term) or verbatim copies of token columns (ProjCol.token) – no arithmetic over tokens (the constant-folded normal form);
• selection atoms are regular comparisons over regular columns, or a comparison of one bare token column against a regular term (the normal form after ProvSQL's normalize_agg_comparison).

Factored annotations and the σ/predsem combination

The row annotation of the general evaluator is kept in factored form GenAnn: a concrete part base : K together with pending, a multiset of group-existence factors – one entry per γ-group whose tokens have not yet been compared, recorded as the group's occurrence-annotation list l and worth δ(⊕ l). The effective annotation of a row is base ⊗ ⊗_{l ∈ pending} δ(⊕ l) (GenAnn.finalize).

This factoring implements the replace-the-δ-factor combination rule:

• Gamma outputs rows with base = 𝟙 and the group's factor pending – an uncompared group row finalizes to δ(⊕ U), as in ProvSQL;
• a selection with aggregate atoms multiplies the predicate provenance predsem(ψ) into base and removes a pending group factor exactly when the compared occurrences are that whole group – every compared token carries the factor's annotation list. In that case the predicate provenance ranges over the non-empty worlds of the very same occurrences, so it subsumes the group-existence factor, and conjoining both would count it twice in a non-idempotent semiring. A predicate comparing tokens of several groups keeps every group factor: its predicate provenance does not entail each group's existence (a disjunction guards only the disjunct that fires), and likewise a predicate that does not entail existence at all (GenPred.entailsExistence – e.g., an aggregate atom ∨-mixed with a regular atom, whose χ can fire in worlds where the group is empty) supersedes nothing. This mirrors ProvSQL's structural supersede (cmp_supersede.cpp with having_entails_group_existence), which drops a δ only when its ⊕-operands are exactly the compared aggregates' occurrence tokens and the predicate entails existence. Annotations accumulated from traversed operators (join partners in base, other groups' pending entries) are always preserved;
• a second selection comparing the same group's tokens finds no pending entry left and simply multiplies: repeated comparisons yield the ⊗-product of their predicate provenances, matching the circuits ProvSQL builds (times of cmp gates) – which coincides with the joint possible-world reading in idempotent semirings;
• a projection dropping the last copy of a token column cashes the group's factor into base (the group can never be compared again).

∧ ↦ ⊗, ∨ ↦ ⊕ and ¬ pushed down to the atoms by De Morgan duality with comparison-operator complementation, exactly as in HavingPred and in ProvSQL. A selection whose predicate contains no aggregate atom filters classically, matching Query.evaluateAnnotated.

Scalar aggregation (aggregation without grouping, whose empty input is a real possible world in ProvSQL) is out of scope: Gamma is the grouped operator only.

inductive ColKind : Type

The kind of a column: a regular value or an aggregate token.

• reg : ColKind
• agg : ColKind
• prov : ColKind

@[instance_reducible]

instance instDecidableEqColKind : DecidableEq ColKind

Equations

• instDecidableEqColKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ColKind.base : ColKind → ColKind

The value-arm kind of a column kind: prov columns hold ordinary values (as ProvSQL's uuid columns do), so their conformance arm is reg.

Equations

• ColKind.agg.base = ColKind.agg
• x✝.base = ColKind.reg

theorem ColKind.base_eq_reg_of_ne_agg {c : ColKind} (h : c ≠ agg) : c.base = reg

@[reducible, inline]

abbrev GenValue (T K : Type) : Type

A lifted column value: a regular value or an aggregate token.

Equations

• GenValue T K = (T ⊕ AggValue T K)

structure GenAnn (K : Type) : Type

The factored annotation of a row of the general evaluator: the concrete part base, and one pending group-existence factor per γ-group whose tokens have not been compared yet, recorded as the group's occurrence-annotation list.

• base : K

  The concrete annotation accumulated so far.

• pending : Multiset (List K)

  The occurrence-annotation lists of the uncompared groups.

def GenAnn.finalize {K : Type} [CommSemiringWithMonus K] (a : GenAnn K) : K

The effective annotation: the concrete part times the pending group-existence factors δ(⊕ l).

Equations

• a.finalize = a.base * (Multiset.map (fun (l : List K) => SemiringWithMonus.delta l.sum) a.pending).prod

@[reducible, inline]

abbrev GenRow (T K : Type) (n : ℕ) : Type

A row of the general evaluator.

Equations

• GenRow T K n = (Tuple (GenValue T K) n × GenAnn K)

@[simp]

theorem GenAnn.finalize_of_pending_zero {K : Type} [CommSemiringWithMonus K] (b : K) : { base := b, pending := 0 }.finalize = b

A row with nothing pending finalizes to its concrete part.

@[simp]

theorem GenAnn.finalize_gamma {K : Type} [CommSemiringWithMonus K] (l : List K) : { base := 1, pending := {l} }.finalize = SemiringWithMonus.delta l.sum

An uncompared γ-row (concrete part 𝟙, its group factor pending) finalizes to δ(⊕ U) – the ProvSQL annotation of a plain GROUP BY output row.

Terms over regular columns

inductive TermG (T : Type) {n : ℕ} (κ : Fin n → ColKind) : Type

A term over the regular columns of a kind-indexed tuple: the index constructor requires its column to be regular, so terms over token columns are unrepresentable.

• const {T : Type} {n : ℕ} {κ : Fin n → ColKind} : T → TermG T κ
• index {T : Type} {n : ℕ} {κ : Fin n → ColKind} (k : Fin n) : κ k = ColKind.reg → TermG T κ
• provIndex {T : Type} {n : ℕ} {κ : Fin n → ColKind} (k : Fin n) : κ k = ColKind.prov → TermG T κ
• cmpAgg {T : Type} {n : ℕ} {κ : Fin n → ColKind} (k : Fin n) : κ k = ColKind.agg → CompOp → TermG T κ → TermG T κ

  The aggregate-comparison gate (ProvSQL's provsql_having): the predicate provenance of comparing the token in column k against the term. Its faithful semantics lives in the rewritten world's term evaluator; the generic evaluators give it a total junk value, and on token-free kinds the constructor is unrepresentable.

• chiGate {T : Type} {n : ℕ} {κ : Fin n → ColKind} : CompOp → TermG T κ → TermG T κ → TermG T κ

  The regular-comparison indicator gate: the characteristic value χ of a comparison between two regular terms – 𝟙 if it holds on the row, 𝟘 otherwise. It is the primitive a HAVING predicate needs for its regular atoms, and like cmpAgg its faithful semantics lives in the rewritten world's term evaluator – the generic evaluators give it a total junk value. Unlike cmpAgg it carries no kind constraint, so it is representable over all-regular columns: the fragment on which the rewritten world's evaluator collapses to the plain semantics is cut out by TermG.chiFree instead.

• add {T : Type} {n : ℕ} {κ : Fin n → ColKind} : TermG T κ → TermG T κ → TermG T κ
• sub {T : Type} {n : ℕ} {κ : Fin n → ColKind} : TermG T κ → TermG T κ → TermG T κ
• mul {T : Type} {n : ℕ} {κ : Fin n → ColKind} : TermG T κ → TermG T κ → TermG T κ

def TermG.eval {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) (u : Tuple (GenValue T K) n) : T

Evaluation of a term on a lifted tuple. On the regular columns the kind index guarantees a regular value; the token arm of collapseSum is never reached on kind-conformant tuples and merely keeps the function total.

Equations

• (TermG.const a).eval u = a
• (TermG.index k a).eval u = AggValue.collapseSum (u k)
• (TermG.provIndex k a).eval u = AggValue.collapseSum (u k)
• (TermG.cmpAgg k a a_1 a_2).eval u = 0
• (TermG.chiGate a a_1 a_2).eval u = 0
• (t₁.add t₂).eval u = t₁.eval u + t₂.eval u
• (t₁.sub t₂).eval u = t₁.eval u - t₂.eval u
• (t₁.mul t₂).eval u = t₁.eval u * t₂.eval u

Generalized selection predicates

inductive GenPred (T : Type) {n : ℕ} (κ : Fin n → ColKind) : Type

A generalized selection predicate: regular comparisons between terms over regular columns, aggregate comparisons of one bare token column against a regular term (the constant-folded normal form), and Boolean structure.

• cmp {T : Type} {n : ℕ} {κ : Fin n → ColKind} : CompOp → TermG T κ → TermG T κ → GenPred T κ

  Regular atom: comparison of two terms over regular columns.

• aggCmp {T : Type} {n : ℕ} {κ : Fin n → ColKind} (k : Fin n) : κ k = ColKind.agg → CompOp → TermG T κ → GenPred T κ

  Aggregate atom: the token in column k compared against a regular term (a per-group constant: query constant or group-key attribute).

• and {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → GenPred T κ → GenPred T κ
• or {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → GenPred T κ → GenPred T κ
• not {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → GenPred T κ

def GenPred.hasAggAtom {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → Bool

Does the predicate contain an aggregate atom? Selections without one filter classically.

Equations

• (GenPred.cmp a a_1 a_2).hasAggAtom = false
• (GenPred.aggCmp k a a_1 a_2).hasAggAtom = true
• (φ.and ψ).hasAggAtom = (φ.hasAggAtom || ψ.hasAggAtom)
• (φ.or ψ).hasAggAtom = (φ.hasAggAtom || ψ.hasAggAtom)
• φ.not.hasAggAtom = φ.hasAggAtom

def GenPred.holds {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K) n) : Prop

Classical (per-tuple) truth of a predicate, reading a compared token through its deterministic collapse. Used by the evaluator only on aggregate-atom-free predicates, where tokens are never consulted.

Equations

• (GenPred.cmp a a_1 a_2).holds u = a.eval (a_1.eval u) (a_2.eval u)
• (GenPred.aggCmp k a a_1 a_2).holds u = a_1.eval (AggValue.collapseSum (u k)) (a_2.eval u)
• (φ_1.and ψ).holds u = (φ_1.holds u ∧ ψ.holds u)
• (φ_1.or ψ).holds u = (φ_1.holds u ∨ ψ.holds u)
• φ_1.not.holds u = ¬φ_1.holds u

def GenPred.decHolds {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K) n) : Decidable (φ.holds u)

Structural decidability of holds.

Equations

• (GenPred.cmp a a_1 a_2).decHolds u = GenPred.decHolds._aux_1 u a a_1 a_2
• (GenPred.aggCmp k a a_1 a_2).decHolds u = GenPred.decHolds._aux_3 u k a a_1 a_2
• (φ_1.and ψ).decHolds u = instDecidableAnd
• (φ_1.or ψ).decHolds u = instDecidableOr
• φ_1.not.decHolds u = instDecidableNot

@[instance_reducible]

instance GenPred.instDecidablePredTupleGenValueHolds {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) : DecidablePred φ.holds

Equations

• φ.instDecidablePredTupleGenValueHolds = φ.decHolds

def GenPred.predsem {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (neg : Bool) (u : Tuple (GenValue T K) n) : K

Predicate provenance of a generalized predicate on a row, with ¬ pushed down to the atoms by De Morgan duality (the neg flag): a regular atom contributes its characteristic value χ, an aggregate atom the predicate provenance predProv of the comparison over its token's group, ∧ ↦ ⊗ and ∨ ↦ ⊕ (swapped under neg), and negated atoms complement their comparison operator, as in ProvSQL.

Equations

• (GenPred.cmp a a_1 a_2).predsem neg u = Having.chi (if neg = true then a.negate else a) (a_1.eval u) (a_2.eval u)
• (GenPred.aggCmp k a a_1 a_2).predsem neg u = match u k with | Sum.inl val => 0 | Sum.inr a => a.predProv (if neg = true then a_1.negate else a_1) (a_2.eval u)
• (φ_1.and ψ).predsem neg u = if neg = true then φ_1.predsem neg u + ψ.predsem neg u else φ_1.predsem neg u * ψ.predsem neg u
• (φ_1.or ψ).predsem neg u = if neg = true then φ_1.predsem neg u * ψ.predsem neg u else φ_1.predsem neg u + ψ.predsem neg u
• φ_1.not.predsem neg u = φ_1.predsem (!neg) u

def GenPred.comparedCols {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → Finset (Fin n)

The token columns compared by the predicate's aggregate atoms.

Equations

• (GenPred.cmp a a_1 a_2).comparedCols = ∅
• (GenPred.aggCmp k a a_1 a_2).comparedCols = {k}
• (φ.and ψ).comparedCols = φ.comparedCols ∪ ψ.comparedCols
• (φ.or ψ).comparedCols = φ.comparedCols ∪ ψ.comparedCols
• φ.not.comparedCols = φ.comparedCols

def GenPred.entailsExistence {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → Bool → Bool

Does the predicate provenance entail the compared groups' existence (under the polarity neg of the enclosing negations)? An aggregate atom does – its predicate provenance ranges over non-empty worlds only – while a regular atom's χ does not. A conjunction (∧ positively, ∨ under negation) entails as soon as one factor does; a disjunction only if every disjunct does. Mirrors ProvSQL's having_entails_group_existence: the supersede of the group-existence factor is licensed only when this holds, since e.g., agg-atom ∨ regular-atom can fire in worlds where the group is empty.

Equations

• (GenPred.cmp a a_1 a_2).entailsExistence x✝ = false
• (GenPred.aggCmp k a a_1 a_2).entailsExistence x✝ = true
• (φ.and ψ).entailsExistence x✝ = if x✝ = true then φ.entailsExistence x✝ && ψ.entailsExistence x✝ else φ.entailsExistence x✝ || ψ.entailsExistence x✝
• (φ.or ψ).entailsExistence x✝ = if x✝ = true then φ.entailsExistence x✝ || ψ.entailsExistence x✝ else φ.entailsExistence x✝ && ψ.entailsExistence x✝
• φ.not.entailsExistence x✝ = φ.entailsExistence !x✝

Projection columns

inductive ProjCol (T : Type) {n : ℕ} (κ : Fin n → ColKind) : Type

One output column of a generalized projection: a regular term over the regular input columns, or a verbatim copy of a token column (no arithmetic over tokens: the normal form).

• term {T : Type} {n : ℕ} {κ : Fin n → ColKind} : TermG T κ → ProjCol T κ
• token {T : Type} {n : ℕ} {κ : Fin n → ColKind} (k : Fin n) : κ k = ColKind.agg → ProjCol T κ
• provTerm {T : Type} {n : ℕ} {κ : Fin n → ColKind} : TermG T κ → ProjCol T κ

def ProjCol.kind {T : Type} {n : ℕ} {κ : Fin n → ColKind} : ProjCol T κ → ColKind

The kind of the output column.

Equations

• (ProjCol.term a).kind = ColKind.reg
• (ProjCol.token k a).kind = ColKind.agg
• (ProjCol.provTerm a).kind = ColKind.prov

def ProjCol.eval {T : Type} [ValueType T] {K : Type} {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol T κ) (u : Tuple (GenValue T K) n) : GenValue T K

Evaluation of a projection column on a lifted tuple.

Equations

• (ProjCol.term a).eval u = Sum.inl (a.eval u)
• (ProjCol.token k a).eval u = u k
• (ProjCol.provTerm a).eval u = Sum.inl (a.eval u)

Kind-indexed queries

def ColKind.allReg (n : ℕ) : Fin n → ColKind

The all-regular kind vector.

Equations

• ColKind.allReg n x✝ = ColKind.reg

inductive AggQuery (T : Type) (n : ℕ) : (Fin n → ColKind) → Type

Kind-indexed general queries. The index discipline enforces the scope conditions: Gamma aggregates an all-regular input, Dedup and Diff require all-regular kinds, and the projection/selection grammars never compute over tokens.

• Rel {T : Type} (n : ℕ) : String → AggQuery T n (ColKind.allReg n)

  Base relation (all-regular).

• Proj {T : Type} {n m : ℕ} {κ : Fin n → ColKind} (ps : Tuple (ProjCol T κ) m) : AggQuery T n κ → AggQuery T m fun (j : Fin m) => (ps j).kind

  Generalized projection.

• Sel {T : Type} {n : ℕ} {κ : Fin n → ColKind} : GenPred T κ → AggQuery T n κ → AggQuery T n κ

  Generalized selection.

• Prod {T : Type} {n₁ n₂ : ℕ} {κ₁ : Fin n₁ → ColKind} {κ₂ : Fin n₂ → ColKind} : AggQuery T n₁ κ₁ → AggQuery T n₂ κ₂ → AggQuery T (n₁ + n₂) (Fin.append κ₁ κ₂)

  Cartesian product (join).

• Sum {T : Type} {n : ℕ} {κ : Fin n → ColKind} : AggQuery T n κ → AggQuery T n κ → AggQuery T n κ

  Union (all).

• Dedup {T : Type} {n : ℕ} : AggQuery T n (ColKind.allReg n) → AggQuery T n (ColKind.allReg n)

  Duplicate elimination – all-regular only.

• Diff {T : Type} {n : ℕ} : AggQuery T n (ColKind.allReg n) → AggQuery T n (ColKind.allReg n) → AggQuery T n (ColKind.allReg n)

  Difference – all-regular only.

• Gamma {T : Type} {m n₁ n₂ : ℕ} (is : Tuple (Fin m) n₁) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) : AggQuery T m (ColKind.allReg m) → AggQuery T (n₁ + n₂) (Fin.append (fun (x : Fin n₁) => ColKind.reg) fun (x : Fin n₂) => ColKind.agg)

  The decomposed grouping operator γ^≼: group the (all-regular) input by the key columns is; one output row per group, carrying the key followed by one aggregate token per (term, aggregate) pair.

• ProvSum {T : Type} {m n₁ : ℕ} {κ : Fin m → ColKind} (is : Tuple (Fin m) n₁) (his : ∀ (k : Fin n₁), κ (is k) ≠ ColKind.agg) (t : TermG T κ) : AggQuery T m κ → AggQuery T (n₁ + 1) (Fin.append (fun (k : Fin n₁) => κ (is k)) fun (x : Fin 1) => ColKind.prov)

  Provenance aggregation: group by the key columns is (none of which may be a token column) and ⊕-sum the term t over each group into a single prov output column – the abstract counterpart of ProvSQL's ⊕-gate creation in rewritten plans.

• Retag {T : Type} {n : ℕ} {κ κ' : Fin n → ColKind} (h : ∀ (k : Fin n), (κ k).base = (κ' k).base) : AggQuery T n κ → AggQuery T n κ'

  Retag value columns between the value-armed kinds (reg and prov): semantically the identity, it declares which value columns carry provenance – the typing act of casting a value column to ProvSQL's uuid type. Token columns cannot be retagged.

• GammaTok {T : Type} {m n₁ n₂ : ℕ} {κ : Fin m → ColKind} (is : Tuple (Fin m) n₁) (his : ∀ (k : Fin n₁), κ (is k) ≠ ColKind.agg) (ts : Tuple (Term T m) n₂) (fs : Tuple (SeqAggFunc T) n₂) (a : TermG T κ) : AggQuery T m κ → AggQuery T (n₁ + n₂ + 1) (Fin.append (Fin.append (fun (k : Fin n₁) => κ (is k)) fun (x : Fin n₂) => ColKind.agg) fun (x : Fin 1) => ColKind.prov)

  Token-building grouping (ProvSQL's provsql_agg): group by the key columns is, output the keys, one aggregate token per (term, aggregate) pair whose occurrence annotations are the values of the explicit annotation term a (in rewritten plans: the provenance column of the subquery), and a trailing prov column carrying the group-existence guard. Its faithful semantics lives in the rewritten world's evaluator; the generic evaluators give it total modeling semantics, and the world-faithfulness exclusions (noProvSum) rule it out of source queries.

def AggQuery.castKind {T : Type} {n : ℕ} {κ κ' : Fin n → ColKind} (h : κ = κ') : AggQuery T n κ → AggQuery T n κ'

Transport a query along an equality of kind vectors (kind vectors arising from projections are rarely definitionally all-regular).

Equations

• AggQuery.castKind h = Eq.rec (motive := fun (x : Fin n → ColKind) (h : κ = x) => AggQuery T n κ → AggQuery T n x) id h

The general evaluator

def GenRow.plainTuple {T K : Type} {n : ℕ} (u : Tuple (GenValue T K) n) : Tuple T n

The regular-value reading of a lifted tuple (token columns collapse; on the all-regular rows fed to Dedup, Diff and Gamma no token occurs).

Equations

• GenRow.plainTuple u k = AggValue.collapseSum (u k)

def GenRow.toAnnotated {T K : Type} [CommSemiringWithMonus K] {n : ℕ} (r : GenRow T K n) : AnnotatedTuple T K n

Finalize a general row into an annotated tuple: collapse the tuple to its regular reading and cash the pending group factors.

Equations

• r.toAnnotated = (GenRow.plainTuple r.1, r.2.finalize)

def GenRow.ofAnnotated {T K : Type} {n : ℕ} (p : AnnotatedTuple T K n) : GenRow T K n

Embed an annotated tuple as a general row (all-regular, nothing pending).

Equations

• GenRow.ofAnnotated p = (fun (k : Fin n) => Sum.inl (p.1 k), { base := p.2, pending := 0 })

def tokenLists {T K : Type} {n : ℕ} (u : Tuple (GenValue T K) n) : Multiset (List K)

The multiset of occurrence-annotation lists of the token columns of a tuple (used by projection to detect dropped groups).

Equations

• tokenLists u = Multiset.filterMap (fun (k : Fin n) => match u k with | Sum.inl val => none | Sum.inr a => some (List.map Prod.snd a.occs)) Finset.univ.val

def TermG.evalPlain {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) (u : Tuple T n) : T

Equations

• (TermG.const a).evalPlain u = a
• (TermG.index k a).evalPlain u = u k
• (TermG.provIndex k a).evalPlain u = u k
• (TermG.cmpAgg k a a_1 a_2).evalPlain u = 0
• (TermG.chiGate a a_1 a_2).evalPlain u = 0
• (t₁.add t₂).evalPlain u = t₁.evalPlain u + t₂.evalPlain u
• (t₁.sub t₂).evalPlain u = t₁.evalPlain u - t₂.evalPlain u
• (t₁.mul t₂).evalPlain u = t₁.evalPlain u * t₂.evalPlain u

The gate-free fragment

The indicator gate TermG.chiGate is the one term constructor whose faithful reading needs the rewritten world: it produces a provenance value out of a comparison between regular values, which the generic evaluators – having no annotation to return – can only approximate by the junk constant. The cmpAgg gate escapes the same fate only because its kind constraint keeps it off the columns the plain semantics sees. The predicates below cut out the fragment where no indicator gate occurs, on which the rewritten world's evaluator is the plain semantics (AggQuery.evaluateRew_plain).

def TermG.chiFree {n : ℕ} {T' : Type} {κ : Fin n → ColKind} : TermG T' κ → Prop

No indicator gate in a term.

Equations

• (TermG.const a).chiFree = True
• (TermG.index k a).chiFree = True
• (TermG.provIndex k a).chiFree = True
• (TermG.cmpAgg k a a_1 t).chiFree = t.chiFree
• (TermG.chiGate a a_1 a_2).chiFree = False
• (t₁.add t₂).chiFree = (t₁.chiFree ∧ t₂.chiFree)
• (t₁.sub t₂).chiFree = (t₁.chiFree ∧ t₂.chiFree)
• (t₁.mul t₂).chiFree = (t₁.chiFree ∧ t₂.chiFree)

def GenPred.chiFree {n : ℕ} {T' : Type} {κ : Fin n → ColKind} : GenPred T' κ → Prop

No indicator gate in a predicate.

Equations

• (GenPred.cmp a t₁ t₂).chiFree = (t₁.chiFree ∧ t₂.chiFree)
• (GenPred.aggCmp k a a_1 t).chiFree = t.chiFree
• (φ.and ψ).chiFree = (φ.chiFree ∧ ψ.chiFree)
• (φ.or ψ).chiFree = (φ.chiFree ∧ ψ.chiFree)
• φ.not.chiFree = φ.chiFree

def ProjCol.chiFree {n : ℕ} {T' : Type} {κ : Fin n → ColKind} : ProjCol T' κ → Prop

No indicator gate in a projection column.

Equations

• (ProjCol.term t).chiFree = t.chiFree
• (ProjCol.provTerm t).chiFree = t.chiFree
• (ProjCol.token k a).chiFree = True

def AggQuery.evaluate {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} : AggQuery T n κ → AnnotatedDatabase T K → Multiset (GenRow T K n)

The general annotated evaluator. All operators preserve the factored-annotation discipline described in the module docstring.

Equations

• One or more equations did not get rendered due to their size.
• (AggQuery.Rel x✝¹ s).evaluate x✝ = match AnnotatedDatabase.find x✝¹ s x✝ with | none => ∅ | some rn => Multiset.map GenRow.ofAnnotated rn
• (q₁.Sum q₂).evaluate x✝ = q₁.evaluate x✝ + q₂.evaluate x✝
• q.Dedup.evaluate x✝ = Multiset.map GenRow.ofAnnotated ↑↑(groupByKey (Multiset.map GenRow.toAnnotated (q.evaluate x✝)))
• (AggQuery.Retag h q).evaluate x✝ = q.evaluate x✝

def AggQuery.evaluateAnnotated {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T K) : AnnotatedRelation T K n

The final annotated relation computed by a general query: evaluate, then finalize every row.

Equations

• q.evaluateAnnotated d = Multiset.map GenRow.toAnnotated (q.evaluate d)

@[simp]

theorem GenRow.toAnnotated_ofAnnotated {T K : Type} [CommSemiringWithMonus K] {n : ℕ} (p : AnnotatedTuple T K n) : (ofAnnotated p).toAnnotated = p

Embedding then finalizing is the identity on annotated tuples.

The plain evaluator

The classical (per-instance) semantics of a general query: aggregate columns hold the computed aggregate values, and every selection filters classically – including aggregate comparisons, evaluated on the computed values. This is the semantics the data-part adequacy connects to the annotated evaluator through AggValue.collapse (the annotated side keeps classically-failing rows with annotation 𝟘, exactly as ProvSQL emits them, so adequacy is stated on the query stripped of its aggregate selections and differences, stripAgg).

def GenPred.holdsPlain {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple T n) : Prop

Classical truth of a predicate on a regular tuple: aggregate atoms compare the computed aggregate value of their column.

Equations

• (GenPred.cmp a a_1 a_2).holdsPlain u = a.eval (a_1.evalPlain u) (a_2.evalPlain u)
• (GenPred.aggCmp k a a_1 a_2).holdsPlain u = a_1.eval (u k) (a_2.evalPlain u)
• (φ_1.and ψ).holdsPlain u = (φ_1.holdsPlain u ∧ ψ.holdsPlain u)
• (φ_1.or ψ).holdsPlain u = (φ_1.holdsPlain u ∨ ψ.holdsPlain u)
• φ_1.not.holdsPlain u = ¬φ_1.holdsPlain u

def GenPred.decHoldsPlain {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple T n) : Decidable (φ.holdsPlain u)

Structural decidability of holdsPlain.

Equations

• (GenPred.cmp a a_1 a_2).decHoldsPlain u = GenPred.decHoldsPlain._aux_1 u a a_1 a_2
• (GenPred.aggCmp k a a_1 a_2).decHoldsPlain u = GenPred.decHoldsPlain._aux_3 u k a a_1 a_2
• (φ_1.and ψ).decHoldsPlain u = instDecidableAnd
• (φ_1.or ψ).decHoldsPlain u = instDecidableOr
• φ_1.not.decHoldsPlain u = instDecidableNot

@[instance_reducible]

instance GenPred.instDecidablePredTupleHoldsPlain {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) : DecidablePred φ.holdsPlain

Equations

• φ.instDecidablePredTupleHoldsPlain = φ.decHoldsPlain

def ProjCol.evalPlain {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} (p : ProjCol T κ) (u : Tuple T n) : T

Plain evaluation of a projection column.

Equations

• (ProjCol.term a).evalPlain u = a.evalPlain u
• (ProjCol.token k a).evalPlain u = u k
• (ProjCol.provTerm a).evalPlain u = a.evalPlain u

def AggQuery.evaluatePlain {T : Type} [ValueType T] {n : ℕ} {κ : Fin n → ColKind} : AggQuery T n κ → Database T → Relation T n

The plain evaluator: standard multiset semantics, with Gamma computing the aggregate of each group's full occurrence sequence (in the canonical ≼ order of Relation.groupSeq) and every selection filtering classically. Diff is the all-or-nothing difference of Query.evaluate.

Equations

• One or more equations did not get rendered due to their size.
• (AggQuery.Rel x✝¹ s).evaluatePlain x✝ = match Database.find x✝¹ s x✝ with | none => ∅ | some rn => rn
• (AggQuery.Proj ps q).evaluatePlain x✝ = Multiset.map (fun (u : Tuple T n_1) (j : Fin x✝¹) => (ps j).evalPlain u) (q.evaluatePlain x✝)
• (AggQuery.Sel φ q).evaluatePlain x✝ = Multiset.filter φ.holdsPlain (q.evaluatePlain x✝)
• (q₁.Prod q₂).evaluatePlain x✝ = q₁.evaluatePlain x✝ * q₂.evaluatePlain x✝
• (q₁.Sum q₂).evaluatePlain x✝ = q₁.evaluatePlain x✝ + q₂.evaluatePlain x✝
• q.Dedup.evaluatePlain x✝ = Multiset.dedup (q.evaluatePlain x✝)
• (q₁.Diff q₂).evaluatePlain x✝ = Multiset.filter (fun (t : Tuple T x✝¹) => t ∉ q₂.evaluatePlain x✝) (q₁.evaluatePlain x✝)
• (AggQuery.Retag h q).evaluatePlain x✝ = q.evaluatePlain x✝

def AggQuery.stripAgg {T : Type} {n : ℕ} {κ : Fin n → ColKind} : AggQuery T n κ → AggQuery T n κ

Strip a general query of the constructs whose annotated data part keeps rows the classical semantics removes: differences (annotated Diff never removes tuple slots) and selections containing an aggregate atom (the annotated evaluator keeps classically-failing rows annotated 𝟘, as ProvSQL emits them). The data-part adequacy of evaluateAnnotated is stated against the plain evaluation of the stripped query, mirroring Query.stripDiff in Provenance.QueryAdequacy.

Equations

• (AggQuery.Rel x✝ s).stripAgg = AggQuery.Rel x✝ s
• (AggQuery.Proj ps q).stripAgg = AggQuery.Proj ps q.stripAgg
• (AggQuery.Sel φ q).stripAgg = if φ.hasAggAtom = true then q.stripAgg else AggQuery.Sel φ q.stripAgg
• (q₁.Prod q₂).stripAgg = q₁.stripAgg.Prod q₂.stripAgg
• (q₁.Sum q₂).stripAgg = q₁.stripAgg.Sum q₂.stripAgg
• q.Dedup.stripAgg = q.stripAgg.Dedup
• (q₁.Diff a).stripAgg = q₁.stripAgg
• (AggQuery.Gamma is ts fs q).stripAgg = AggQuery.Gamma is ts fs q.stripAgg
• (AggQuery.ProvSum is his t q).stripAgg = AggQuery.ProvSum is his t q.stripAgg
• (AggQuery.Retag h q).stripAgg = AggQuery.Retag h q.stripAgg
• (AggQuery.GammaTok is his ts fs a q).stripAgg = AggQuery.GammaTok is his ts fs a q.stripAgg

def AggQuery.noProvSum {T : Type} {n : ℕ} {κ : Fin n → ColKind} : AggQuery T n κ → Prop

No plan-level provenance aggregation. The possible-world metatheorems (random-world commutation, PQE) are about source queries; ProvSum is a rewriting-target operator whose deterministic group sum is not world-faithful – exactly as the classical Agg was excluded from the annotated evaluators.

Equations

• (AggQuery.Rel x✝ s).noProvSum = True
• (AggQuery.Proj ps q).noProvSum = q.noProvSum
• (AggQuery.Sel φ q).noProvSum = q.noProvSum
• (q₁.Prod q₂).noProvSum = (q₁.noProvSum ∧ q₂.noProvSum)
• (q₁.Sum q₂).noProvSum = (q₁.noProvSum ∧ q₂.noProvSum)
• q.Dedup.noProvSum = q.noProvSum
• (q₁.Diff a).noProvSum = (q₁.noProvSum ∧ a.noProvSum)
• (AggQuery.Gamma is ts fs q).noProvSum = q.noProvSum
• (AggQuery.ProvSum is his t q).noProvSum = False
• (AggQuery.Retag h q).noProvSum = q.noProvSum
• (AggQuery.GammaTok is his ts fs a q).noProvSum = False

Kind conformance

Rows produced by the general evaluator conform to the query's kind vector: regular columns hold regular values, token columns hold tokens. This is an invariant lemma, not a hypothesis: the kind-indexed syntax makes it hold by construction, and downstream theorems (the random-world commutation in particular) invoke it instead of assuming wellformedness.

def GenValue.kindOf {T K : Type} : GenValue T K → ColKind

The kind of a lifted value.

Equations

• GenValue.kindOf (Sum.inl val) = ColKind.reg
• GenValue.kindOf (Sum.inr a) = ColKind.agg

theorem AggQuery.evaluate_conform {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T K) (r : GenRow T K n) : r ∈ q.evaluate d → ∀ (k : Fin n), (r.1 k).kindOf = (κ k).base

Kind conformance of the general evaluator.

Home · Documentation · Publications · Contributors · Source · Cite