Relations read as families of occurrences

An annotated relation is a multiset of annotated tuples, so two copies of a tuple carrying the same annotation are one element with multiplicity two: nothing tells them apart. That is the right reading for most of the algebra, where an operator treats equal rows equally.

Three things need more. An operator may give two equal rows different results – a window frame that excludes the row it is computed for reads its twin and not itself, so the two rows get different aggregate values from the same relation. A comparison may read two aggregate values whose occurrence families overlap, and then the worlds it sums over are subfamilies of their union, which needs an occurrence of one family to be recognizable as an occurrence of the other. And a statement about an operator may quantify over the ways equal rows could be told apart, which is how one shows that no operator selecting rows can have the behavior of EXCEPT ALL.

This module gives the finer reading: a relation as a family indexed by occurrences, where the index is the identity a multiset discards. It does not replace AnnotatedRelation; it sits beside it, with toMultiset forgetting the index. An operator defined on families is meaningful exactly when its result does not depend on which indexing was chosen, which is what Congr below expresses.

structure OccFam (α : Type) : Type

A relation read as a family of occurrences: size of them, each a row of type α. Two copies of a row are two occurrences, told apart by their index, and an aggregate value built from this relation names its occurrences by the same index – which is what lets two such values speak of the same occurrence.

The row type is a parameter because the rows a window produces are not the rows it reads: it appends an aggregate column, so its output rows carry a token where its input rows carry only values.

• size : ℕ

  How many occurrences the family has.

• row : Fin self.size → α

  The occurrence at each index.

theorem List.Perm.exists_get_equiv {α : Type} {l₁ l₂ : List α} (h : l₁.Perm l₂) : ∃ (e : Fin l₁.length ≃ Fin l₂.length), ∀ (i : Fin l₁.length), l₂.get (e i) = l₁.get i

A permutation of lists gives a bijection of positions carrying one to the other. Mathlib states this for lists without repeats (List.Nodup.getEquiv); relations have repeats, so it is proved here by induction on the permutation, each case building the bijection from the one before.

def OccFam.toMultiset {α : Type} (r : OccFam α) : Multiset α

Forgetting the index: the multiset of rows the family stands for.

Equations

• r.toMultiset = Multiset.map r.row Finset.univ.val

def OccFam.nil {α : Type} : OccFam α

The empty family.

Equations

• OccFam.nil = { size := 0, row := fun (i : Fin 0) => i.elim0 }

def OccFam.Congr {α : Type} (r r' : OccFam α) : Prop

Two families index the same relation when a bijection of their indices matches their occurrences. This is the relation an operator on families has to respect: the choice of index is not data, only the occurrences are.

Equations

• r.Congr r' = ∃ (e : Fin r.size ≃ Fin r'.size), ∀ (i : Fin r.size), r'.row (e i) = r.row i

A relation read as a family

An operator on families is meaningful when it respects Congr. To apply one to a relation, a relation has to be read as a family, which means choosing an indexing. ofMultiset chooses one; toMultiset_ofMultiset says the choice is faithful, and Congr_of_toMultiset_eq says any two choices are the same family, so that an operator respecting Congr gives an answer that does not depend on the choice.

noncomputable def OccFam.ofMultiset {α : Type} (s : Multiset α) : OccFam α

A choice of indexing for a multiset.

Equations

• OccFam.ofMultiset s = { size := s.toList.length, row := fun (i : Fin s.toList.length) => s.toList.get i }

theorem OccFam.Congr_of_toMultiset_eq {α : Type} {r r' : OccFam α} (h : r.toMultiset = r'.toMultiset) : r.Congr r'

Any two indexings of a relation are the same family. Two families with the same multiset of rows differ by a permutation of their indices, so an operator that respects Congr answers the same on both, and reading a relation as a family involves no arbitrary choice.

This is the standard fact that a permutation of lists gives a bijection of positions carrying one to the other, which Mathlib does not appear to state for lists with repeats. Nothing below depends on it for its definition, only for the claim that the definition is about relations rather than about indexings.

Home · Documentation · Publications · Contributors · Source · Cite