An evaluation reads its context only where it says it does

AggQueryIn.readsOuter lists the context positions a query reads. This file proves that the annotated evaluation depends on the context – the valuation γ of the parameters and the environment's context of general values – only at those positions, provided every operator building aggregate values records the positions its subtree reads (AggQueryIn.readsRecorded), which is what it stamps its values with (AggQueryIn.evaluate_congr_reads).

This is what makes an operator's values a function of their family identifier: two evaluations of one operator under contexts that agree on the parameters it records build the same values.

def AgreeOn {c : ℕ} {α : Type} (r : Fin c → Bool) (γ γ' : Fin c → α) : Prop

Two valuations agree on the positions a read set holds.

Equations

• AgreeOn r γ γ' = ∀ (k : Fin c), r k = true → γ k = γ' k

The values an operator builds read the parameters only through its terms

The congruence

theorem AggQueryIn.evaluate_congr_reads {T : Type} [ValueType T] {K : Type} [CommSemiringWithMonus K] [DecidableEq K] [HasAltLinearOrder K] {c n : ℕ} {κ : Fin n → ColKind} {l : List (String × ℕ)} (q : AggQueryIn T c n κ l) : q.readsRecorded → ∀ (d : AnnotatedDatabase T K) {γ γ' : Fin c → T} {E E' : EvalEnv T K}, (∀ p ∈ l, E.holes p.1 p.2 = E'.holes p.1 p.2) → AgreeOn q.readsOuter γ γ' → AgreeOn q.readsOuter (E.ctxAt c γ) (E'.ctxAt c γ') → q.evaluate d γ E = q.evaluate d γ' E'

An evaluation reads its context only where it says it does. Two valuations of the parameters and two environment contexts that agree on the positions the query reads, with the same rounds bound to the names it reads, give the same evaluation – provided the operators building aggregate values record the positions their subtrees read, which is what they stamp.

Home · Documentation · Publications · Contributors · Source · Cite