Possible-world foundations for the general evaluator

The token-level ingredients of the random-world commutation for AggQuery.evaluate over 𝔹[X] (the general-evaluator counterpart of randomWorld_evaluateAnnotated, whose target statement is

genRandomWorld v (q.evaluate d) = q.evaluatePlain (d.randomWorld v)

– under a valuation v, specializing the general evaluation's surviving rows is the plain evaluation of the realized world):

• AggValue.realized – the positions of a token's occurrences realized by a valuation, and AggValue.specialize_eval connecting the world-faithful reading specialize to the per-world reading valOn at the realized world;
• AggValue.predProv_eval_iff – the token-level PQE bridge: under a valuation, the predicate provenance of a comparison against a token is true iff the realized group is non-empty and its aggregate value satisfies the comparison. This is havingProv_eval_iff transported to tokens; the σ-aggregate case of the commutation reduces to it;
• GenRow.specializeTuple and genRandomWorld – the specialized reading of a row and the realized world of a general evaluation: the rows whose finalized annotation is true, with tokens specialized.

def AggValue.realized {T X : Type} (a : AggValue T (BoolFunc X)) (v : X → Bool) : Finset (Fin a.occs.length)

The positions of a token's occurrences realized by a valuation.

Equations

• a.realized v = {i : Fin a.occs.length | a.anns i v = true}

theorem AggValue.specialize_eval {T X : Type} (a : AggValue T (BoolFunc X)) (v : X → Bool) : (a.specialize fun (α : BoolFunc X) => α v) = a.valOn (a.realized v)

The world-faithful reading under a valuation is the per-world reading at the realized world.

theorem AggValue.predProv_eval_iff {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] (a : AggValue T (BoolFunc X)) (op : CompOp) (c : T) (v : X → Bool) : a.predProv op c v = true ↔ (a.realized v).Nonempty ∧ op.eval (a.specialize fun (α : BoolFunc X) => α v) c

The token-level PQE bridge. Under a valuation v, the predicate provenance of ⟨token⟩ op c is true iff the token's realized group is non-empty and its specialized aggregate value satisfies the comparison. The σ-aggregate case of the random-world commutation reduces to this.

def GenValue.specializeAt {T X : Type} (v : X → Bool) : GenValue T (BoolFunc X) → T

The specialized reading of a lifted value: regular values are themselves, a token aggregates its realized occurrences.

Equations

• GenValue.specializeAt v = Sum.elim id fun (a : AggValue T (BoolFunc X)) => a.specialize fun (α : BoolFunc X) => α v

def GenRow.specializeTuple {T X : Type} {n : ℕ} (v : X → Bool) (u : Tuple (GenValue T (BoolFunc X)) n) : Tuple T n

The specialized reading of a row's tuple.

Equations

• GenRow.specializeTuple v u k = GenValue.specializeAt v (u k)

def genRandomWorld {T X : Type} {n : ℕ} (v : X → Bool) (R : Multiset (GenRow T (BoolFunc X) n)) : Multiset (Tuple T n)

The realized world of a general evaluation: the rows whose finalized annotation is true under the valuation, with tokens specialized.

Equations

• genRandomWorld v R = Multiset.map (fun (r : GenRow T (BoolFunc X) n) => GenRow.specializeTuple v r.1) (Multiset.filter (fun (r : GenRow T (BoolFunc X) n) => r.2.finalize v = true) R)

Evaluation of factored annotations

def annGuard {X : Type} (l : List (BoolFunc X)) (v : X → Bool) : Prop

Truth of a group's existence guard under a valuation: some occurrence annotation is realized.

Equations

• annGuard l v = ∃ κ ∈ l, κ v = true

@[instance_reducible]

instance instDecidableAnnGuard {X : Type} (l : List (BoolFunc X)) (v : X → Bool) : Decidable (annGuard l v)

Equations

• instDecidableAnnGuard l v = instDecidableAnnGuard._aux_1 l v

theorem GenAnn.finalize_eval_iff {X : Type} (a : GenAnn (BoolFunc X)) (v : X → Bool) : a.finalize v = true ↔ a.base v = true ∧ ∀ l ∈ a.pending, annGuard l v

Pointwise truth of a finalized factored annotation: the concrete part holds and every pending group is realized non-empty (δ is the identity on 𝔹[X]).

theorem AggValue.annGuard_iff_realized {T X : Type} (a : AggValue T (BoolFunc X)) (v : X → Bool) : annGuard (List.map Prod.snd a.occs) v ↔ (a.realized v).Nonempty

A token's existence guard is the non-emptiness of its realized world.

Specialized readings under kind conformance

theorem GenValue.eq_inl_of_kindOf_reg {T K' : Type} {x : GenValue T K'} (h : x.kindOf = ColKind.reg) : ∃ (w : T), x = Sum.inl w

A regular-kinded value is a left injection.

theorem GenValue.eq_inr_of_kindOf_agg {T K' : Type} {x : GenValue T K'} (h : x.kindOf = ColKind.agg) : ∃ (a : AggValue T K'), x = Sum.inr a

A token-kinded value is a right injection.

theorem TermG.eval_specialize {T : Type} [ValueType T] {X : Type} {n : ℕ} {κ : Fin n → ColKind} (t : TermG T κ) (u : Tuple (GenValue T (BoolFunc X)) n) (hconf : ∀ (k : Fin n), (u k).kindOf = (κ k).base) (v : X → Bool) : t.eval u = t.evalPlain (GenRow.specializeTuple v u)

On a kind-conformant tuple, a term's lifted evaluation is its plain evaluation on the specialized tuple (regular columns hold regular values, on which both readings are the identity).

theorem GenPred.holds_iff_specialize {T : Type} [ValueType T] {X : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (hφ : φ.hasAggAtom = false) (u : Tuple (GenValue T (BoolFunc X)) n) (hconf : ∀ (k : Fin n), (u k).kindOf = (κ k).base) (v : X → Bool) : φ.holds u ↔ φ.holdsPlain (GenRow.specializeTuple v u)

On a kind-conformant tuple, an aggregate-atom-free predicate holds iff its plain reading holds on the specialized tuple.

The σ-aggregate row lemma

def GenPred.selCompared {T K' : Type} {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K') n) : Multiset (List K')

The annotation lists of the tokens compared by a predicate on a row (the evaluator's compared).

Equations

• φ.selCompared 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)) φ.comparedCols.val

def GenPred.selPending {T K' : Type} [DecidableEq K'] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T K') n) (p : Multiset (List K')) : Multiset (List K')

The pending factors after a σ with aggregate atoms (the evaluator's update, definitionally).

Equations

• φ.selPending u p = if φ.entailsExistence false = true then Multiset.filter (fun (l : List K') => ¬(φ.selCompared u ≠ 0 ∧ ∀ l' ∈ φ.selCompared u, l' = l)) p else p

theorem GenPred.predsem_eval_iff {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (neg : Bool) (u : Tuple (GenValue T (BoolFunc X)) n) (hconf : ∀ (k : Fin n), (u k).kindOf = (κ k).base) (v : X → Bool) (hg : ∀ k ∈ φ.comparedCols, ∀ (a : AggValue T (BoolFunc X)), u k = Sum.inr a → (a.realized v).Nonempty) : φ.predsem neg u v = true ↔ if neg = true then ¬φ.holdsPlain (GenRow.specializeTuple v u) else φ.holdsPlain (GenRow.specializeTuple v u)

Predicate provenance evaluation, under existence guards. On a kind-conformant row all of whose compared groups are realized non-empty, the predicate provenance is true iff the (polarity-adjusted) plain predicate holds on the specialized tuple.

theorem GenPred.entails_guard {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (neg : Bool) (u : Tuple (GenValue T (BoolFunc X)) n) (v : X → Bool) (ℓ₀ : List (BoolFunc X)) (huni : ∀ k ∈ φ.comparedCols, ∀ (a : AggValue T (BoolFunc X)), u k = Sum.inr a → List.map Prod.snd a.occs = ℓ₀) (hent : φ.entailsExistence neg = true) (hp : φ.predsem neg u v = true) : annGuard ℓ₀ v

Existence entailment extracts the guard. When a predicate entails existence and all its compared tokens carry the annotation list ℓ₀, a true predicate provenance realizes ℓ₀.

Finalize algebra (any m-semiring)

theorem GenAnn.finalize_cash {K' : Type} [CommSemiringWithMonus K'] [DecidableEq K'] (b : K') (p kept : Multiset (List K')) (hle : kept ≤ p) : { base := b * (Multiset.map (fun (l : List K') => SemiringWithMonus.delta l.sum) (p - kept)).prod, pending := kept }.finalize = { base := b, pending := p }.finalize

Cashing pending factors into the concrete part preserves the finalized annotation (the projection case of the evaluator).

theorem GenAnn.finalize_mul {K' : Type} [CommSemiringWithMonus K'] (a₁ a₂ : GenAnn K') : { base := a₁.base * a₂.base, pending := a₁.pending + a₂.pending }.finalize = a₁.finalize * a₂.finalize

The finalized annotation of a product row is the product of the finalized annotations.

The row-level σ lemmas

theorem GenPred.sel_finalize_old {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T (BoolFunc X)) n) (b : BoolFunc X) (p : Multiset (List (BoolFunc X))) (v : X → Bool) (h : { base := b * φ.predsem false u, pending := φ.selPending u p }.finalize v = true) : { base := b, pending := p }.finalize v = true

A σ with aggregate atoms only strengthens the annotation: the finalized updated annotation implies the finalized original one (the superseded factors are recovered from the predicate provenance through existence entailment).

theorem GenPred.sel_finalize_eval_iff {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] {n : ℕ} {κ : Fin n → ColKind} (φ : GenPred T κ) (u : Tuple (GenValue T (BoolFunc X)) n) (b : BoolFunc X) (p : Multiset (List (BoolFunc X))) (v : X → Bool) (hconf : ∀ (k : Fin n), (u k).kindOf = (κ k).base) (hguard : { base := b, pending := p }.finalize v = true → ∀ (k : Fin n) (a : AggValue T (BoolFunc X)), u k = Sum.inr a → (a.realized v).Nonempty) : { base := b * φ.predsem false u, pending := φ.selPending u p }.finalize v = true ↔ { base := b, pending := p }.finalize v = true ∧ φ.holdsPlain (GenRow.specializeTuple v u)

The σ-aggregate row lemma. On a kind-conformant, guarded row, the updated annotation is realized iff the original annotation is realized and the plain predicate holds on the specialized tuple.

The guardedness invariant

theorem AggQuery.evaluate_guarded {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] [HasAltLinearOrder (BoolFunc X)] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T (BoolFunc X)) (r : GenRow T (BoolFunc X) n) : r ∈ q.evaluate d → ∀ (v : X → Bool), r.2.finalize v = true → ∀ (k : Fin n) (a : AggValue T (BoolFunc X)), r.1 k = Sum.inr a → (a.realized v).Nonempty

Guardedness of the general evaluator: on any row it produces, whenever the finalized annotation is realized, every token's group is realized non-empty – the group-existence guard of each token is carried either by a pending factor or by a predicate provenance in the concrete part.

Realized-world plumbing

The Gamma case helpers

The random-world commutation

theorem AggQuery.genRandomWorld_evaluate {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] [HasAltLinearOrder (BoolFunc X)] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (_hq : q.noProvSum) (d : AnnotatedDatabase T (BoolFunc X)) (v : X → Bool) : genRandomWorld v (q.evaluate d) = q.evaluatePlain (AnnotatedDatabase.randomWorld v d)

Random-world commutation for the general evaluator (over 𝔹[X]): specializing the realized rows of the general annotated evaluation is the plain evaluation of the realized world. The σ-aggregate case is the row lemma GenPred.sel_finalize_eval_iff under the conformance and guardedness invariants; the Gamma case rests on groupSeq_randomWorld.

Unrestricted probabilistic query evaluation (PQE)

noncomputable def AggQuery.booleanProv {T : Type} [ValueType T] {X : Type} [HasAltLinearOrder (BoolFunc X)] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (d : AnnotatedDatabase T (BoolFunc X)) : BoolFunc X

The Boolean provenance of a general query: the ⊕-sum of the finalized annotations of its rows – true in a world iff some row is realized.

Equations

• q.booleanProv d = (Multiset.map (fun (r : GenRow T (BoolFunc X) n) => r.2.finalize) (q.evaluate d)).sum

theorem AggQuery.booleanProv_eval_iff {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] [HasAltLinearOrder (BoolFunc X)] {n : ℕ} {κ : Fin n → ColKind} (q : AggQuery T n κ) (hq : q.noProvSum) (d : AnnotatedDatabase T (BoolFunc X)) (v : X → Bool) : q.booleanProv d v = true ↔ q.evaluatePlain (AnnotatedDatabase.randomWorld v d) ≠ 0

Pointwise PQE bridge, general form: the Boolean provenance of a general query is true in a world iff the plain evaluation of that world is non-empty. Immediate from the random-world commutation.

noncomputable def AggQuery.booleanProb {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] {n : ℕ} {κ : Fin n → ColKind} (P : ProbAssignment X) (q : AggQuery T n κ) (d : AnnotatedDatabase T (BoolFunc X)) : ℚ

Probability that a random world of d satisfies the Boolean query q (non-empty answer), over a tuple-independent probabilistic database.

Equations

• AggQuery.booleanProb P q d = ∑ v : X → Bool, if Multiset.card (q.evaluatePlain (AnnotatedDatabase.randomWorld v d)) = 0 then 0 else P.valProb v

theorem AggQuery.boolean_pqe {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] [HasAltLinearOrder (BoolFunc X)] {n : ℕ} {κ : Fin n → ColKind} (P : ProbAssignment X) (q : AggQuery T n κ) (hq : q.noProvSum) (d : AnnotatedDatabase T (BoolFunc X)) : booleanProb P q d = P.funcProb (q.booleanProv d)

Unrestricted probabilistic query evaluation. For any general query – aggregate comparisons anywhere, through joins, projections, unions and further selections – over a tuple-independent probabilistic database, the probability that a random world satisfies the Boolean query equals the probability of its Boolean provenance. This removes the top-level restriction of the fused booleanHaving_pqe.

noncomputable def AggQuery.tupleProv {T : Type} [ValueType T] {X : Type} [HasAltLinearOrder (BoolFunc X)] {n : ℕ} (q : AggQuery T n (ColKind.allReg n)) (d : AnnotatedDatabase T (BoolFunc X)) (t : Tuple T n) : BoolFunc X

The provenance of a tuple t in a general query with all-regular output: the ⊕-sum of the finalized annotations of the rows whose data part is t.

Equations

• q.tupleProv d t = (Multiset.map (fun (r : GenRow T (BoolFunc X) n) => r.2.finalize) (Multiset.filter (fun (r : GenRow T (BoolFunc X) n) => GenRow.plainTuple r.1 = t) (q.evaluate d))).sum

theorem AggQuery.tupleProv_eval_iff {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] [HasAltLinearOrder (BoolFunc X)] {n : ℕ} (q : AggQuery T n (ColKind.allReg n)) (hq : q.noProvSum) (d : AnnotatedDatabase T (BoolFunc X)) (t : Tuple T n) (v : X → Bool) : q.tupleProv d t v = true ↔ t ∈ q.evaluatePlain (AnnotatedDatabase.randomWorld v d)

Pointwise tuple-marginal bridge: the provenance of t is true in a world iff t belongs to the plain evaluation of that world.

noncomputable def AggQuery.tupleProb {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] {n : ℕ} (P : ProbAssignment X) (q : AggQuery T n (ColKind.allReg n)) (d : AnnotatedDatabase T (BoolFunc X)) (t : Tuple T n) : ℚ

The marginal probability that t belongs to a random world's answer.

Equations

• AggQuery.tupleProb P q d t = ∑ v : X → Bool, if t ∈ q.evaluatePlain (AnnotatedDatabase.randomWorld v d) then P.valProb v else 0

theorem AggQuery.tuple_pqe {T : Type} [ValueType T] {X : Type} [Fintype X] [DecidableEq X] [HasAltLinearOrder (BoolFunc X)] {n : ℕ} (P : ProbAssignment X) (q : AggQuery T n (ColKind.allReg n)) (hq : q.noProvSum) (d : AnnotatedDatabase T (BoolFunc X)) (t : Tuple T n) : tupleProb P q d t = P.funcProb (q.tupleProv d t)

Unrestricted tuple-marginal PQE: for a general query with all-regular output over a tuple-independent probabilistic database, the marginal probability of an answer tuple is the probability of its provenance. This is the general-evaluator counterpart of the classical intensional-PQE theorem ProbAssignment.theorem_12, with aggregate comparisons allowed anywhere in the query.

Home · Documentation · Publications · Contributors · Source · Cite