def r : Relation String 4

Equations

• One or more equations did not get rendered due to their size.

def d : Database String

Equations

• d = [("Personnel", ⟨4, r⟩)]

def qPersonnel : Query String 4

Equations

• qPersonnel = Query.Rel 4 "Personnel"

def q₀ : Query String (Nat.succ 0)

Equations

• q₀ = ε (Π ![#3] qPersonnel)

def q₁ : Query String (Nat.succ 0)

Equations

• One or more equations did not get rendered due to their size.

def q₂ : Query String (Nat.succ 0)

Equations

• q₂ = (q₀ - q₁)

def r_count : AnnotatedRelation String ℕ 4

Equations

• r_count = Relation.annotate (fun (x : Tuple String 4) => 1) r

def d_count : AnnotatedDatabase String ℕ

Equations

• d_count = [("Personnel", ⟨4, r_count⟩)]

def r_tropical : AnnotatedRelation String (Tropical (WithTop ℕ)) 4

Equations

• r_tropical = Relation.annotate (fun (x : Tuple String 4) => Tropical.trop 1) r

def d_tropical : AnnotatedDatabase String (Tropical (WithTop ℕ))

Equations

• d_tropical = [("Personnel", ⟨4, r_tropical⟩)]

The general (kind-indexed) syntax and its rewriting

The same database, now through AggQuery: aggregation, HAVING, and the rewriting of both into the composite domain String ⊕ ℕ.

def qgPersonnel : AggQuery String 4 (ColKind.allReg 4)

Equations

• qgPersonnel = AggQuery.Rel 4 "Personnel"

def qgCount : AggQuery String (Nat.succ 0 + Nat.succ 0) (Fin.append (fun (x : Fin (Nat.succ 0)) => ColKind.reg) fun (x : Fin (Nat.succ 0)) => ColKind.agg)

Equations

• qgCount = AggQuery.Gamma ![3] ![Term.const "1"] ![SeqAggFunc.sum] qgPersonnel

def φexactlyTwo : GenPred String (ColKind.gammaKinds 1 1)

Equations

• φexactlyTwo = (GenPred.fusedCmp CompOp.ge 0 (Term.const "2")).and (GenPred.fusedCmp CompOp.le 0 (Term.const "2"))

def φatLeastThree : GenPred String (ColKind.gammaKinds 1 1)

Equations

• φatLeastThree = GenPred.fusedCmp CompOp.ge 0 (Term.const "3")

def cityCols : Tuple (ProjCol String (ColKind.gammaKinds 1 1)) 1

Equations

• cityCols x✝ = ProjCol.term (TermG.index (Fin.castAdd 1 0) cityCols._proof_1)

def qgAllCities : AggQuery String 1 (ColKind.allReg 1)

Equations

• qgAllCities = AggQuery.Proj cityCols qgCount

def qgBigCities : AggQuery String 1 (ColKind.allReg 1)

Equations

• qgBigCities = AggQuery.Proj cityCols (AggQuery.Sel φatLeastThree qgCount)

def qgSmallCities : AggQuery String 1 (ColKind.allReg 1)

Equations

• qgSmallCities = qgAllCities.Diff qgBigCities

def qgCountRew : AggQuery (String ⊕ ℕ) 3 (ColKind.gammaRewKinds 1 1)

Equations

• qgCountRew = AggQuery.gammaRew ![3] ![Term.const "1"] ![SeqAggFunc.sum] qgPersonnel trivial

def qgHavingRew : AggQuery (String ⊕ ℕ) 3 (ColKind.gammaRewKinds 1 1)

Equations

• qgHavingRew = AggQuery.havingPredRew ![3] ![Term.const "1"] ![SeqAggFunc.sum] φexactlyTwo qgPersonnel trivial

def φbigOrBerlin : GenPred String (ColKind.gammaKinds 1 1)

Equations

• φbigOrBerlin = (GenPred.fusedCmp CompOp.ge 0 (Term.const "3")).or (GenPred.cmp CompOp.eq (TermG.index (Fin.castAdd 1 0) cityCols._proof_1) (TermG.const "Berlin"))

def qgMixedRew : AggQuery (String ⊕ ℕ) 3 (ColKind.gammaRewKinds 1 1)

Equations

• qgMixedRew = AggQuery.havingPredRew ![3] ![Term.const "1"] ![SeqAggFunc.sum] φbigOrBerlin qgPersonnel trivial

Home · Documentation · Publications · Contributors · Source · Cite