Congruence of predicate provenance under tie-block permutations

The occurrence payload of an aggregate token is produced by Having.havingGroup, which sorts the group by the canonical order on the tuple part and breaks ties on equal tuple parts by an arbitrary fixed order on the annotations. Pushing a semiring homomorphism through the annotated database can therefore reorder the payload – but only within blocks of occurrences with equal tuple parts, hence equal aggregated-term values.

This file proves that the predicate provenance of a token is invariant under exactly such reorderings. The invariance is genuinely limited to tie blocks: for an order-sensitive aggregate, exchanging two occurrences of equal value across an occurrence of a different value changes the predicate provenance.

• TiePerm eqv – permutations generated by transposing adjacent elements related by eqv (here: pairs with equal first components), the guarded analogue of List.Perm;
• tiePerm_of_perm_of_sorted – two lists that are permutations of each other and both sorted by a common key are related by TiePerm on key equality;
• AggValue.predProvAux – a recursion form of the predicate provenance, with accumulators for the values kept so far, the annotations discarded so far, and whether the world is already non-empty;
• AggValue.predProv_eq_predProvAux – the world-sum of AggValue.predProv equals the recursion form;
• AggValue.predProv_congr – the congruence: tokens with the same aggregate and TiePerm-related payloads have the same predicate provenance.

Tie-block permutations

inductive TiePerm {α : Type} (eqv : α → α → Prop) : List α → List α → Prop

Permutations generated by transposing adjacent elements related by eqv: the guarded analogue of List.Perm, whose swap constructor requires the exchanged elements to be related. For eqv the equality of sort keys, this captures exactly the reorderings a sort with an arbitrary tie-break can introduce.

• nil {α : Type} {eqv : α → α → Prop} : TiePerm eqv [] []
• cons {α : Type} {eqv : α → α → Prop} (a : α) {l₁ l₂ : List α} : TiePerm eqv l₁ l₂ → TiePerm eqv (a :: l₁) (a :: l₂)
• swap {α : Type} {eqv : α → α → Prop} {a b : α} (h : eqv a b) {l₁ l₂ : List α} : TiePerm eqv l₁ l₂ → TiePerm eqv (a :: b :: l₁) (b :: a :: l₂)
• trans {α : Type} {eqv : α → α → Prop} {l₁ l₂ l₃ : List α} : TiePerm eqv l₁ l₂ → TiePerm eqv l₂ l₃ → TiePerm eqv l₁ l₃

theorem TiePerm.refl {α : Type} (eqv : α → α → Prop) (l : List α) : TiePerm eqv l l

theorem TiePerm.symm {α : Type} {eqv : α → α → Prop} (hsymm : ∀ {a b : α}, eqv a b → eqv b a) {l₁ l₂ : List α} : TiePerm eqv l₁ l₂ → TiePerm eqv l₂ l₁

theorem TiePerm.perm {α : Type} {eqv : α → α → Prop} {l₁ l₂ : List α} (h : TiePerm eqv l₁ l₂) : l₁.Perm l₂

A tie-block permutation is in particular a permutation.

theorem TiePerm.map {α β : Type} {eqv : α → α → Prop} {eqv' : β → β → Prop} (g : α → β) (hg : ∀ {a b : α}, eqv a b → eqv' (g a) (g b)) {l₁ l₂ : List α} : TiePerm eqv l₁ l₂ → TiePerm eqv' (List.map g l₁) (List.map g l₂)

Tie-block permutations transport along maps that preserve the guard.

theorem TiePerm.map_fst_eq {γ δ : Type} {l₁ l₂ : List (γ × δ)} (h : TiePerm (fun (p q : γ × δ) => p.1 = q.1) l₁ l₂) : List.map Prod.fst l₁ = List.map Prod.fst l₂

On lists of pairs with equal first components as guard, a tie-block permutation leaves the sequence of first components unchanged (whereas an unrestricted permutation would only preserve it as a multiset).

Sorted permutations are tie-block permutations

theorem tiePerm_cons_erase {α κ : Type} [DecidableEq α] [LinearOrder κ] (key : α → κ) {l : List α} {p : α} : p ∈ l → List.Pairwise (fun (x y : α) => key x ≤ key y) l → (∀ q ∈ l, key p ≤ key q) → TiePerm (fun (x y : α) => key x = key y) l (p :: l.erase p)

Bubbling a minimal element of a sorted list to the front only ever transposes adjacent elements of equal key.

theorem tiePerm_of_perm_of_sorted {α κ : Type} [DecidableEq α] [LinearOrder κ] (key : α → κ) {l₁ l₂ : List α} : l₁.Perm l₂ → List.Pairwise (fun (x y : α) => key x ≤ key y) l₁ → List.Pairwise (fun (x y : α) => key x ≤ key y) l₂ → TiePerm (fun (x y : α) => key x = key y) l₁ l₂

Two lists that are permutations of each other and both sorted by the key key differ only by a tie-block permutation on key equality: the sort order determines everything except the arrangement inside blocks of equal keys.

Position bookkeeping for the world split

The recursion form of predicate provenance

def AggValue.predProvAux {T K : Type} [ValueType T] [CommSemiringWithMonus K] (f : SeqAggFunc T) (op : CompOp) (c : T) : List T → K → Bool → List (T × K) → K

Recursion form of the predicate provenance of a token: acc accumulates the values of the occurrences kept so far, ex the sum of the annotations of the occurrences discarded so far, and started records whether an occurrence has been kept (worlds must end up non-empty). Keeping an occurrence contributes its annotation as a factor; discarding it moves its annotation into the pending 𝟙 ⊖ Σ factor materialized at the end of the list.

Equations

• AggValue.predProvAux f op c x✝² x✝¹ x✝ [] = if x✝ = true then (1 - x✝¹) * Having.chi op (f x✝²) c else 0
• AggValue.predProvAux f op c x✝² x✝¹ x✝ ((v, a) :: t) = a * AggValue.predProvAux f op c (x✝² ++ [v]) x✝¹ true t + AggValue.predProvAux f op c x✝² (x✝¹ + a) x✝ t

theorem AggValue.sum_worlds_eq_predProvAux {T K : Type} [ValueType T] [CommSemiringWithMonus K] (f : SeqAggFunc T) (op : CompOp) (c : T) (l : List (T × K)) (acc : List T) (ex : K) (started : Bool) : ∑ W : Finset (Fin l.length) with started = true ∨ W.Nonempty, (∏ i ∈ W, (l.get i).2) * ((1 - (ex + ∑ i ∈ Wᶜ, (l.get i).2)) * Having.chi op (f (acc ++ List.map Prod.fst (Having.seqOf l W))) c) = predProvAux f op c acc ex started l

The world-sum defining the predicate provenance, generalized by the three accumulators, equals the recursion form.

theorem AggValue.predProv_eq_predProvAux {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] (a : AggValue T K) (op : CompOp) (c : T) : a.predProv op c = predProvAux a.agg op c [] 0 false a.occs

The predicate provenance of a token is its recursion form.

theorem AggValue.predProvAux_congr {T K : Type} [ValueType T] [CommSemiringWithMonus K] (f : SeqAggFunc T) (op : CompOp) (c : T) {l₁ l₂ : List (T × K)} (h : TiePerm (fun (p q : T × K) => p.1 = q.1) l₁ l₂) (acc : List T) (ex : K) (started : Bool) : predProvAux f op c acc ex started l₁ = predProvAux f op c acc ex started l₂

The recursion form is invariant under tie-block permutations of the payload: exchanging two adjacent occurrences with equal values redistributes the same annotations over the same world readings.

theorem AggValue.predProv_congr {T K : Type} [ValueType T] [CommSemiringWithMonus K] [DecidableEq K] {a b : AggValue T K} (hagg : a.agg = b.agg) (h : TiePerm (fun (p q : T × K) => p.1 = q.1) a.occs b.occs) (op : CompOp) (c : T) : a.predProv op c = b.predProv op c

Congruence of predicate provenance: tokens with the same aggregate whose payloads differ by a tie-block permutation on equal values have the same predicate provenance, for every comparison. This is what makes the annotation tie-break of the group sort semantically invisible.

theorem AggValue.collapse_congr {T K : Type} {a b : AggValue T K} (hagg : a.agg = b.agg) (h : TiePerm (fun (p q : T × K) => p.1 = q.1) a.occs b.occs) : a.collapse = b.collapse

The deterministic reading of a token only depends on the value sequence, which a tie-block permutation preserves.

theorem AggValue.annSum_congr {T K : Type} [CommSemiringWithMonus K] {a b : AggValue T K} (h : TiePerm (fun (p q : T × K) => p.1 = q.1) a.occs b.occs) : (List.map Prod.snd a.occs).sum = (List.map Prod.snd b.occs).sum

The sum of the occurrence annotations of a token is invariant under any permutation of the payload, in particular a tie-block one.

Home · Documentation · Publications · Contributors · Source · Cite