Title: Theory / Important / CS / Algo / Database / Cosette

Definition: The type of tuples with attributes \(\sigma\)
Page: 3
Variables: \(\sigma\) a set of attributes
Context: HotTSQL
Notation: Tuple(\(\sigma\))

Name: A \(K\)-relation
Definition: A function \(\texttt{Tuple}\sigma\to K\) with finite support
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
Context: HotTTSQL
Example: A bag
Example2: A set
Denoted by: [$]\llbracket R\rrbracket[/$]
Applied to: \(\mathbb N\)-relation
Applied to2: \(\mathbb B\)-relation

Definition: [$]\lambda t. \llbracket R\rrbracket t + \llbracket S\rrbracket t[/$]
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R, S\) some \(K\)-relations
Context: HotTTSQL
Notation: [$]\llbracket R\texttt{ UNION ALL }S\rrbracket[/$]

Definition: [$]\lambda (t1, t2)\llbracket R\rrbracket t_1 \times \llbracket S\rrbracket t_2[/$]
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R, S\) some \(K\)-relations
Context: HotTTSQL
Notation: [$]\llbracket \texttt{SELECT * FROM } R x, S y\rrbracket[/$]

Definition: [$]\lambda (t)\llbracket R\rrbracket t \times \llbracket b\rrbracket t[/$]
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R, S\) some \(K\)-relations
Context: HotTTSQL
Notation: [$]\llbracket\texttt{SELECT * FROM } R x, \texttt{ WHERE }b\rrbracket [/$]

Definition: [$$]\lambda t_2\sum_{t1\in\texttt{Tuple}\sigma_1}(\llbracket a_2\rrbracket t_1=\llbracket a_1\rrbracket t_1)\times \llbracket R\rrbracket t_1[/$$]
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R, S\) some \(K\)-relations
Context: HotTTSQL
Notation: [$]\llbracket
\texttt{SELECT $x.a_1$ as $a_2$ FROM $R$ $x$}\rrbracket[/$]

Definition: [$$]\lambda t.\norm{\llbracket R\rrbracket t}[/$$]
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R, S\) some \(K\)-relations
Context: HotTTSQL
Notation: [$]\llbracket
\texttt{DISTINCT $R$ }\rrbracket[/$]

Definition: \(1_K\) if \(b\) holds on \(t\) otherwise \(0_K\)
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(b\) a predicate
\(t\in\texttt{Tuple}\sigma\)
Context: HotTTSQL
Notation: [$]\llbracket b\rrbracket t[/$]

Definition: The projection of \(t\) on the entry \(a\)
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(t\in\texttt{Tuple}\sigma\)
\(a\in\sigma\)
Context: HotTTSQL
Notation: [$]\llbracket a\rrbracket t[/$]

Name: The squash of \(k\)
Definition: \(0_K\) if \(k = 0_K\), otherwise \(1_k\)
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(k\in K\)
Context: HotTTSQL
Notation: [$]\parallel k\parallel[/$]

Definition: \(1_K\) if \(k_1 = k_2\), otherwise \(0_k\)
Page: 3
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(k_1, k_2\in K\)
Context: HotTTSQL
Notation: \((k_1 = k_2)\)

Definition: The class of homotopy type
Page: 3
Context: HotTTSQL
Notation: \(\mathcal U\)

Question: What is the usual problem with formal proof in SQL
Answer: the theory holds only for finite relation. Hence each step of proofs of equality must prove finiteness of terms
Page: 3
Context: HotTTSQL

Question: How to deal with the fact that SQL formalism only deal with finite relation
Answer: work in a theory that allow potentially infinite relation. If a sequence of equality starts with a finite relation and equality holds over arbitrary relation, then the last term will also be finite
Page: 3
Context: HotTTSQL

Name: A HOTT-relation
Page: 4
Context: HotTTSQL
Name2: A \(\mathcal U\)-relation

Name: A concrete schema
Definition: A schema whose all attributes are known
Page: 5
Context: HotTTSQL

Name: A generic schema
Definition: A schema with some unknown attributes
Page: 5
Context: HotTTSQL

Name: A HotTTSQL program
Definition: A list of statements
Page: 5
Denoted by: \(h\)

Name: A statement
Definition: a declaration
Page: 5
Context: HotTTSQL
Definition2: a verify statement
Conjdef: either
Denoted by: \(s\)

Name: A verify statement
Definition: A pair of SQL queries whose equivalence is to be checked
Page: 5
Context: HotTTSQL

Question: The kind of declaration
Answer: schema
Page: 5
Context: HotTTSQL
Answer2: table
Answer3: predicate
Answer4: function
Answer5: aggregate

Name: An attribute
Page: 6
Context: HotTTSQL
Denoted by: \(a\)

Name: A projection
Definition: *
Page: 6
Context: HotTTSQL
Definition2: \(x.*\) for \(x\) a TableAlias
Conjdef: either
Definition3: \(e\mathtt{ AS }a\) for \(e\) an expression and \(a\) an attribute
Definition4: \(p_1,p_2\) for \(p_1\) and \(p_2\) projections
Denoted by: \(p\)

Name: An expression
Definition: \(x.a\) for \(x\) a TableAlias and \(a\) an attribute
Page: 6
Context: HotTTSQL
Definition2: \(f(e_1,\dots,e_n)\) for \(f\) an \(n\)-ary function and \(e_i\) some expressions
Conjdef: either
Definition3: \(\alpha(q)\) for \(\alpha\) an aggregation predicate and \(q\) a query
Denoted by: \(e\)

Name: A predicate
Definition: \(e_1=e_2\) for \(e_1,e_2\) expressions
Page: 6
Context: HotTTSQL
Definition2: TRUE and FALSE
Conjdef: either
Definition3: Boolean combination of predicates
Definition4: \(\beta(x_1,\dots,x_n)\) for \(\beta\) a \(n\)-ary predicate and \(x_i\) some TableAlias
Denoted by: \(b\)
Definition5: \(\mathtt{EXISTS } q\) for \(q\) a query

Name: A TableAlias
Page: 6
Context: HotTTSQL
Denoted by: \(x\)

Name: A query
Definition: \(t\) for \(t\) a
Page: 6
Context: HotTTSQL
Definition2: \(\mathtt{SELECT }p q\) for \(p\) a projection and \(q\) a query
Conjdef: Either
Definition3: \(\mathtt{FROM }q_1 x_1, \dots, x_n x_n\) for \(q_i\) queries and \(x_i\) TableAlias
Definition4: \(q\mathtt{ WHERE }p\) for \(q\) a query and \(p\) a projection
Denoted by: \(q\)
Definition5: \(q_1\texttt{ UNION ALL } q_2\) for \(q_1, q_2\) queries
Definition6: \(q_1\texttt{ EXCEPT }q_2\) for \(q_1,q_2\) queries
Definition7: \(\mathtt{DISTINCT } q\) for \(q\) a query

Name: A declaration
Definition: schema \(\sigma(a_1:\tau _1,\dots, a_n: \tau_n, ??)\) for \(a_i\) attributes
Page: 6
Context: HotTTSQL
Definition2: table \(t(\sigma)\) for \(\sigma\) a schema
Conjdef: Either
Definition3: predicate \(\beta(\sigma_1,\dots,\sigma_n)\) for \(\sigma_i\) schemas
Definition4: function \(f(e_1,\dots,e_n):\tau\)
Denoted by: \(s\)
Definition5: aggregate \(\alpha(\sigma):\tau\) for \(\sigma\) a schema

Name: The squash types
Definition: \(\mathbf 0\) and \(\mathbf 1\)
Page: 6
Variables: \((\mathcal U, \mathbf{0}, \mathbf 1, +, \times, \dot\to\mathbf 0,\parallel\dot\parallel,\sum)\)
Context: HotTTSQL

Definition: [$$]\lambda t.(\llbracket R\rrbracket t)\times ((\llbracket S\rrbracket t)\to 0)[/$$]
Page: 6
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R, S\) some \(K\)-relations
Context: HotTTSQL
Notation: [$]\llbracket R\texttt{ EXCEPT }S\rrbracket[/$]

Name: The negation of \(k\)
Definition: \(1_K\) if \(k=0_K\), \(0_K\) otherwise
Page: 6
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(k\in K\)
Context: HotTTSQL
Notation: \(k\to\mathbf 0\)

Definition: [$$]\lambda t.\sum_{t':\texttt{Tuple}\sigma_R}\parallel\llbracket k\rrbracket t'=t\parallel \times\llbracket R\rrbracket t'[/$$]
Page: 7
Variables: \(\sigma\) a set of attributes
\(K\) a semi ring
\(R\) a relation
\(k\) an expression
Context: HotTTSQL
Notation: [$]\llbracket \texttt{SELECT k FROM } R\rrbracket[/$]

Page: 7
Implementation: SELECT * FROM R x = SELECT x.* FROM R x, R y WHERE x.k = y.k
Section: 3.4
Language: SQL
Returns: the value k is unique in R
Context: Cosette (hence, for proof, not actual implementation)
Instruction: key k(R)
Intuition: \(k\) is a key of \(R\)

Page: 7
Section: 3.4
Language: SQL
Returns: SELECT DISTINCT k as k, α(  SELECT x.a AS a FROM R x WHERE x.k = y.k) AS a_1 FROM R y
Context: Cosette
Instruction: SELECT k as k, α(x.a) AS a_1 FROM R x GROUP BY x.k

Page: 7
Implementation: key a(DISTINCT SELECT x.a AS a, x.a AS b from R x)
Section: 3.4
Name: functional  dependency from a to b
Language: SQL
Returns: Whether for each tuple \(t_1\) and \(t_2\) in \(R\) with \(t_1.a=t_2.a\) we have \(t_1.b=t_2.b\)
Context: Cosette
Instruction: fd a -> b in R
Etymology: b is the result of a function applied to a and R

Question: How are type represented in Cosette
Answer: As binary tree
Page: 8
Section: 3.4
Context: Cosette
Construction: If you take the product of types \(\sigma_1\) and \(\sigma_2\), a binary tree allow you to access to \(\sigma_2\) without knowing anything about \(\sigma_1\) while a list would require to know \(\sigma_1\)'s length

Page: 11
Implementation: SELECT * FROM A x WHERE EXISTS (SELECT * FROM B y WHERE θ(x, y))
Section: 3.4
Name: θ-semijoin
Language: SQL
Returns: Content of A satisfiying θ(a, b) for some B b
Context: Cosette
Instruction: A SEMIJOIN B ON θ