Véronique Benzaken
email: veronique.benzaken@lri.fr

Évelyne Contejean
email: evelyne.contejean@lri.fr

A Coq Mechanised Formal Semantics for Realistic SQL Queries * Formally Reconciling SQL and Bag Relational Algebra

Keywords: CCS Concepts, Information systems → Relational database query languages;, Theory SQL, Formal Semantics, Coq

In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of select [distinct] from where group by having queries with NULL values, functions, aggregates, quantifiers and nested potentially correlated sub-queries. Relying on the Coq extraction mechanism to Ocaml, we further produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all wellknown algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra.

Introduction

Providing a formal semantics for a language is a tricky but crucial task as it allows compilers to rigorously reason about program behaviours and to verify the correctness of optimisations [START_REF] Harper | Practical Foundations for Programming Languages[END_REF]18]. When considering real-life programming languages the task becomes even harder as it happens that the specifications of the language are often written in natural language. Even when they are formal, they only account for a limited subset of the considered language and are, most of the time, human-checked proven correct. In all cases, there are few strong guarantees that the whole faithfully accounts for the exact semantics and correctness of performed optimisations. As the standard for relational database management systems (RDBMS's), SQL is widely and intensively used and does not escape these drawbacks.

To obtain such high level guarantees, a promising approach consists in using proof assistants such as Coq [START_REF]The Coq Proof Assistant Reference Manual[END_REF] or Isabelle [START_REF]The Isabelle Interactive Theorem Prover[END_REF] to define mechanised, executable semantics whose correctness is machine-checkable. A shining demonstration of the viability of this undertaking for real systems is Leroy's CompCert project [START_REF] Leroy | A Formally Verified Compiler Back-end[END_REF].

Our long-term goal, based on the same methodology, aims at providing a Coq verified compiler for SQL. In this article we focus on semantic issues and define, using Coq, a formal semantics for SQL. SQL's Specificities Over time, the search for such a formal semantics has been pursued by the database community. However only restricted fragments of the language were handled. This is due, in particular, to SQL's specificities.

SQL's main construct consists in the select from where group by having block. It is well known that SQL's select from where enjoys a bag semantics, the same element may occur several times in the result, while purely set-theoretic operators such as ∪ (union), ∩ (intersect) and \ (except) have a set-theoretic one. Any formal semantics must account for both sets and bags.

It is notorious that SQL deals with NULL values that are intended to represent unknown information. This aspect, considered of major difficulty in the database field, has to be accurately handled by any mechanised semantics.

SQL queries involve functions (+,-,...) and aggregates (sum, max, count,...) that are intensively used namely when the group by having clause is present.

Last, SQL allows for nested sub-queries, i.e., queries gathering different select's, and more importantly correlated Related Works As relational algebra [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF] plays for SQL the same role as (a combinator version of) λ-calculus for functional programming languages, obviously, early proposals, among those [START_REF] Ceri | Translating SQL into Relational Algebra: Optimisation, Semantics, and Equivalence of SQL Queries[END_REF][START_REF] Negri | Formal Semantics of SQL Queries[END_REF], presented a translation from SQL to such an algebra (see [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF] for a survey). Only a subset of SQL (with no functions, nested queries, NULL's nor bags though) was addressed. The first semantics for SQL accounting for NULL's and bags is found in [START_REF] Guagliardo | A Formal Semantics of SQL Queries, Its Validation, and Applications[END_REF]. However, the work does not consider group by having clauses, aggregates, quantifiers in formulae nor complex expressions: their expressions are restricted to attributes' names or constants. As will be shown in Section 2 and 3, the treatment of complex expressions is very subtle.

On the proof assistant side, the first attempt to formalise relational algebra, using the Agda proof assistant [START_REF]The Agda Proof Assistant Reference Manual[END_REF], is found in [START_REF] Gonzalia | Towards a Formalisation of Relational Database Theory in Constructive Type Theory[END_REF][START_REF] Gonzalia | Relations in Dependent Type Theory[END_REF] while the first, almost complete, Coq formalisation of the relational model in which the data model, algebra, tableaux queries, the chase as well as integrity constraints aspects were modelled, is found in [START_REF] Benzaken | A Coq Formalization of the Relational Data Model[END_REF].

The very first attempt to verify, using Coq, a RDBMS is presented in [START_REF] Malecha | Toward a Verified Relational Database Management System[END_REF]. However the SQL fragment considered is a reconstruction of SQL in which attributes are denoted by positions. They did not deal with group by having clauses, quantifiers in formulae, nested, correlated queries neither NULL's nor aggregates. As we shall see in Section 2 and 3 the treatment of attributes' names and more generally environments in the presence of correlated sub-queries is a particularly, if not the most, tough task. Recently, in [START_REF] Chu | HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics[END_REF], a tool to decide whether two SQL queries are equivalent is presented. To do so, the authors defined HottSQL, a Krelation [START_REF] Green | Provenance semirings[END_REF] based semantics for SQL which handles the select from where fragment with aggregates but without having. Like [START_REF] Malecha | Toward a Verified Relational Database Management System[END_REF], they used a reconstruction of the language thus not accounting for the trickier aspects of variable binding. Last, and more importantly, their semantics is not executable hence it is impossible to verify whether they do implement SQL's semantics. Finally, the closest proposal in terms of mechanised semantics for SQL is addressed in [START_REF] Auerbach | Handling Environments in a Nested Relational Algebra with Combinators and an Implementation in a Verified Query Compiler[END_REF]. A mere translation from SQL to a Coq modelisation of the nested relational algebra (NRA [START_REF] Cluet | Nested Queries in Object Bases[END_REF]) which directly serves as a semantics for SQL is proposed. However, as NRA's syntax significantly deviates from SQL's one, convincing oneself of the accuracy of the proposed semantics is not immediate.

Contributions In this article we give five contributions. We provide (i) SQL Coq , a Coq internalisation of SQL's syntax together with its mechanised executable bag semantics. Our formalisation accounts for select [distinct] from where group by having queries with NULL values, functions, aggregates, quantifiers and nested potentially correlated subqueries. By doing so, thanks to the Coq extraction mechanism to Ocaml, we produce (ii) a Coq certified semantic analyser for the compiler. We then formalise, using Coq, (iii) SQL Alg , a bag, environment-aware relational algebra similar to, while extending it, the one presented in [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF]. By formally relating SQL Coq to SQL Alg , through a Coq mechanised translation, and by formally proving that these translations preserve semantics, we not only are able to (iv) recover all well-known algebraic equivalences on which are based most of compilers' optimisations but we also (v) establish the first, to our best knowledge, mechanised, formal proof of equivalence between the considered SQL fragment and bag relational algebra.

Organisation In Section 2, we first present SQL and SQL's subtleties that need to be taken into account to provide a correct semantics. Then we detail, in Section 3, SQL Coq 's syntax and semantics. Section 4 is devoted to the mechanisation of SQL Alg , the bag algebra. Then the translations between SQL Coq and SQL Alg as well as the equivalence theorem are presented. We conclude, draw lessons and give perpectives in Section 5.

SQL: Simple and Complex

As a domain-specific declarative language SQL is often considered simple.

SQL in a Nutshell

SQL operates over collections of tuples. Tuples are labelled records whose components range over atomic types (integers, strings, etc). In this context labels are called attributes. Such attributes are denotable and may be used within expressions built thanks to functions and accumulators which are called aggregates. SQL's main construct consists in select e from q where c1 group by e' having c2.

For instance select a+2 as a', max(c) as mc from t where b>3 group by a having sum(c) = 0 is a typical SQL query where a,b,c are attributes, sum, max are aggregates, + a function and b>3 a condition.

In order to evaluate a block, inner query q is evaluated, then filtered against boolean condition c1. This intermediate result is so-called "grouped" using expressions e'; meaning that all elements of a group are homogeneously evaluated over e', and groups are maximal w.r.t. inclusion. Then groups are filtered against boolean condition c2, and expressions e are evaluated over remaining groups, yielding the final tuples. On the example above, assuming that the evaluation of t yields (a=1;b=1;c=4), (a=1;b=5;c=2), (a=1;b=4;c=-2), (a=3;b=5;c=1), (a=3;b=4;c=2)

The filtering step against b>3 gives (a=1;b=5;c=2), (a=1;b=4;c=-2), (a=3;b=5;c=1), (a=3;b=4;c=2)

The grouping step w.r.t. a provides {(a=1;b=5;c=2), (a=1;b=4;c=-2)}, {(a=3;b=5;c=1), (a=3;b=4;c=2)} The filtering step against sum(c)=0 discards the last group for which sum(c) = 3 and keeps only the first group. The evaluation of a+2, max(c) yields the result {(a'=3;mc=2)}.

Inside SQL

Yet, SQL's semantics is more subtle than appears at first sight. It is described by the ISO Standard [START_REF]Information technology -Database Languages -SQL -Part 2: Foundation (SQL/Foundation)[END_REF] which is difficult to exploit as:

• it consists of thousand pages hence it is complex to find where features are described (most of the time a single piece of information is spread over the whole document) • when described, features are depicted in a verbose way (for instance definition of the OCaml equivalent of map takes several pages) • last, even abundant, it is often under-specified.

For all those reasons it cannot serve as a formal semantics. This also explains why many vendors implement various aspects of it in their own way as witnessed by [START_REF] Arvin | Comparison of different SQL's implementations[END_REF]. Of course, we relied on the Standard _ as much as possible _ and meanwhile we tested our development against systems like PostgreSQL and Oracle™ to better grasp SQL's semantics.

In the remainder of this article, we note [[q]] the result of the evaluation of query q, () the tuple constructor, [ ] the list constructor, { } the set constructor and {| | } the bag constructor. Figure 1 gathers a bunch of queries that will illustrate SQL's most subtle aspects.

NULL Values

SQL deals with NULL values that are intended to represent unknown information. A 3-valued logic combined with the classical Boolean logic is used to handle them. However NULL's are not treated in a uniform way according to the context as we illustrate in this section.

The first query returns {|(b = 3); (b = NULL)|} thus exemplifying that NULL behaves as an absorbing element for functions 1 . The next three queries, borrowed from [START_REF] Guagliardo | A Formal Semantics of SQL Queries, Its Validation, and Applications[END_REF], exemplify the fact that NULL is neither equal to nor different from any 1 Except for Boolean functions in PostgreSQL.

other value (including itself): comparing NULL with any expression always yields unknown. Query Q2 returns an empty result. This is explained by the fact that [[select s.a from s]] = {|(s.a=NULL)| } , hence [[r.a not in select s.a from s]] (where in is the membership predicate) yields not unknown, that is unknown, over all tuples (r.a=x), in particular over (r.a=1) and (r.a=NULL). This condition is eventually considered as false, therefore neither tuple belongs to the result of query Q2.

Query Q3 returns {|(r.a=1); (r.a=NULL)| }. Let subQ3 be the sub-query (select * from s where s.a = r.a), it yields an empty result over all tuples (r.a=x), hence [[exists (subQ3)]], where exists stands for the non emptyness predicate, is always false and [[not exists (subQ3)]] is always true, thus (r.a=1) and (r.a=NULL) are in the result of Q3.

Query Q4 returns {(r.a=1)}, because the set difference does not use 3-valued logical equality, but standard syntactic equality. Here both tuples (r.a=NULL) and (s.a=NULL) are equal. The main concern is to precisely detect when SQL falls from 3-valued logic into usual Boolean logic. It appears that whereas the evaluation of formulae is performed in the 3-valued logic, when using them as filtering conditions (either where or having) usual Boolean logic is used (unknown becomes false). This will be detailed in Figure 7 and Figure 8 of Section 3.

Last, query Q5 returns {|(t.a=NULL,c=2); (t.a=1,c=1)| }. This illustrates the fact that NULL, which is neither equal nor different from NULL in a 3-valued logic, is indeed equal to NULL in the context of grouping. The semantics proposed in Section 3.2 will account for such behaviours.

Correlated Sub-queries

Let us now address the way SQL manages evaluation environments in presence of aggregates and nested correlated queries. In order to evaluate simple (without aggregates) expressions, it is enough to have a single environment, containing information about the bound attributes and the values for them. In this simple case (e.g., select a1, b1 from t1;) such an environment corresponds to a unique tuple (a1=x,b1=y) where x and y range in the active domains of a1 and b1 respectively.

Evaluating expressions with aggregates is more involved, since an aggregate operates over a list of values, each one corresponding to a tuple. The crucial point is to understand how such a list of tuples, that we call an evaluation context, is produced. Section 10.9 of [START_REF]Information technology -Database Languages -SQL -Part 2: Foundation (SQL/Foundation)[END_REF] (< aggregate functions >, how to retrieve the rows -page 545) should provide some guidance in answering this question. Unfortunately it was of no help. Taking advantage of Coq's execution mechanism we rather decided to run queries over a small database of our own. We thus proceeded by testing many queries over Post-greSQL, Oracle™ and against our formal semantics. Relying on a mechanised and executable semantics was essential as it compelled us to examine in details all sub-cases. It took us significant effort to reach the semantically relevant set of queries which are given in Figure 1. For all of them, we obtained the same results on all three systems. Let us comment on these queries. For Q6 the result is:

r a 1 NULL s a NULL t a 1 NULL NULL t 1 a 1 b 1 1 1 1 2 1 3 1 4 1 5 a 1 b 1 1 6 1 7 1 8 1 9 1 10 a 1 b 1 2 1 2 2 2 3 2 4 2 5 a 1 b 1 2 6 2 7 2 8 2 9 2 10 a 1 b 1 3 1 3 2 3 3 3 4 3 5
(a1=1,m=10); (a1=2,m=10); (a1=3,m=5); (a1=4,m=10)

It is easy to understand what happens when evaluating max( b1) in Q6: each group (where a1 is fixed) contains some tuples, each of them yielding a value for b1. Then max is computed over this list of values. For instance, the group T 1 where a1=1 contains exactly one occurence of tuples of the form (a1=1,b1=i), where i ranges from 1 to 10, hence b1 ranges from 1 to 10, and max(b1) is equal to 10, whereas the group where a1=3 contains tuples (a1=3,b1=i), where i=1,...,5, and max(b1) is equal to 5. In this simple case a group merely yields an evaluation context -we say that the group has been split into individual tuples. The situation gets more complex when evaluating an aggregate expression in a nested sub-query. How to build, in that case, the suitable evaluation contexts in order to get the needed lists of values, arguments of the aggregate? The last queries of Figure 1: Q7,Q8,Q9,Q10,Q11,Q12,Q13,Q14 and table t2 have been designed to answer this question. Note that all are correlated queries except Q7 and Q9 which are simply nested. These queries follow the same pattern: select a1 from t1 group by a1 having exists (select a2 from t2 group by a2 having e=k);

Assuming that an aggregate expression occurs in a subquery under more than two grouping levels, as e in the above pattern, there are several groups in the environment. In our example, homogeneous groups w.r.t. a1 are the following:

𝒢 1 =                10 i=1 {|(a1=1;b1=i)| } 10 i=1 {|(a1=2;b1=i)| } 5 i=1 {|(a1=3;b1=i)| } 10 i=6 {|(a1=4;b1=i)| }               
whereas there is a single homogeneous group w.r.t. a2, T 2 = {|(a2=7;b2=7); (a2=7;b2=7)| }. Thus global environment for the innermost expression e is made of T 2 and one T 1 of 𝒢 1 denoted by: [T 2 ;T 1 ].

T 1 T 2
How to combine these groups in order to obtain the correct evaluation context (i.e., the one actually used by SQL on PostgreSQL and Oracle™)? Which groups must be split and which must not?

Let us consider Q7(k) where the innermost filtering condition is sum(1+0

*a2) = k. When k 2 [[Q7(k)]
] is empty, and for k = 2 it is equal to i=4 i=1 {|(a1=i)| }. Expression sum(1+0*a2) actually computes the number of tuples in the evaluation context and this number is equal to 2 for all groups T 1 of 𝒢 1 : combining T 1 and T 2 yields a context containing two (the cardinality of T 2 ) tuples, whatever the cardinality of T 1 . We have to draw the conclusion that when evaluating sum(1+0*a2) = k, T 2 has been split whereas T 1 is not used at all.

T 1 T 2
Let us now examine correlated query Q8(k), which is very similar to Q7(k), except that the filtering con- [START_REF] Gonzalia | Relations in Dependent Type Theory[END_REF]]] = {|(a1=1); (a1=2)| }. Hence expression sum (1+0*a1) computes the cardinality of T 1 . When evaluating sum(1+0*a1) = k, T 1 has been split, whereas T 2 is not used.

dition is sum(1+0*a1) = k. When k {5, 10} [[Q8(k)]] is empty while [[Q8(5)]] = {|(a1=3); (a1=4)| } and [[Q8
T 1 T 2
Fact 1. In the same environment, [T 2 ;T 1 ], SQL either splits T 1 or T 2 in order to build an evaluation context from which evaluation of aggregate expressions is performed. The expression to be evaluated directs the way the evaluation context is built by choosing which relevant group to split into: T 1 for 1+0*a1, and T 2 for 1+0*a2. At that point it seems that this choice is guided by attributes (a1 or a2).

Thus, the next interesting case is when there are no attributes in the expression under the aggregate as in Q9(k). What should be the relevant group to be split into? Is there even such a relevant group for sum(1)? Actually Q9(k) yields the same result as Q7(k), meaning that the relevant group for a constant is the innermost group T 2 . Fact 2. In the very same environment, 1+0*a2 is equal to 1 and 1+0*a1 is not since these expressions are computed in different evaluation contexts: under aggregates, in SQL, usual arithmetic equalities are no longer valid.

At that point, what happens if both expressions 1+0*a1

and 1+0*a2 have to be evaluated in the same environment as it is the case for Q10(k), where 1+0*a1 and 1+0*a2 occur under distinct aggregates? There is no single obvious relevant group anymore. When k {7, 12} [[Q10(k)]] is empty while [[Q10 [START_REF] Cluet | Nested Queries in Object Bases[END_REF]]] = {|(a1=3); (a1=4)| } and [[Q10 [START_REF] Guagliardo | A Formal Semantics of SQL Queries, Its Validation, and Applications[END_REF]]] = {|(a1=1); (a1=2)| }, meaning that both expressions 1+0*a1 and 1+0*a2 have been evaluated independently, the first in a context where T 1 has been split into, and the second where the split group is T 2 . Fact 3. This makes clear that SQL allows two sub-expressions of a given expression to be evaluated in different contexts which is definitely contrary to what is done in other mainstream programming languages! What if 1+0*a1 and 1+0*a2 occur under the same aggregate, as in

Q11(k)? When k=2, [[Q11(2)]] is i=4 i=1 {|(a1=i)| }, otherwise [[Q11(k)]] is empty. Fact 4.
Therefore T 2 , the innermost relevant group, has been split into. T 1 has been collapsed to any of its elements t 1 since only its homogeneous part, a1, is used by the evaluation.

t 1 T 2
As the reader may have noticed, all expressions under the aggregates were built upon grouping attributes. What happens when such is not the case? Query Q12(k) contains sum(1+0*a1+0*b2) and behaves exactly the same as Q11(k) does. Query Q13(k) contains sum(1+0*b1+0*b2) and is not well formed according to the Standard, thus, is not evaluated. The reason is that under the aggregate there are two non grouping attributes coming from different nesting levels. The last query, Q14(k), which contains sum(1+0*b1+0*a2), is also ill-formed and not evaluated. However one could imagine that it could have been accepted and evaluated in the following context:

T 1 t 2
At that point, we are able to sum up the lessons above and precisely explain how SQL manages environments.

Summary

First, when evaluating an expression with aggregates where the top operator is a function (for instance +, as in Q10(k)), each argument is evaluated separately.

Second, when evaluating an expression ag(e) where the top operator ag is an aggregate, this aggregate is evaluated over a list of values. The subtle point is to understand how to build the suitable evaluation context to retrieve such values. Let us clarify the previously discussed notions.

Complete Environments A complete environment, ℰ = [S n ; ...; S 1 ], is a stack of slices: one slice per nesting level i, the innermost level being on the top. When necessary, we shall equally adopt the following notation for environments ℰ = (A, G,T ) :: ℰ ′ in order to highlight the list's head. Slices are of the form S = (A, G,T ), where A (also noted A(S)) contains the relevant attributes for that level of nesting, i.e., the names introduced in the subquery at this level2 ; G the grouping expressions appearing in the group by (also noted G(S)); and T a non empty list of tuples3 (also noted T (S)).

S n S n-1 S 1
Evaluation Contexts When e is a constant expression, the list of tuples T (S n ) comes from the innermost slice of environment ℰ = [S n ; ...; S 1 ]. In the simple case where all attributes of e are introduced at the same level i, the relevant list is simply T (S i ). Otherwise, when attributes of e belong to at least two different levels, the innermost (i.e., of greatest index) being S k , there are two cases:

• either the expression is not well-formed (cf Q13 and Q14), because e contains an expression of T (S j ), j < k which is not grouped. • or the expression e is exactly built upon the attributes corresponding to the kth level and the grouping expressions 4 of outermost levels k -1, . . . , 1. In this case, let t j be a fixed tuple chosen in each T (S j ) for j < k, then the list of relevant tuples is made of the concatenations (t; t k -1 ; . . . ; t 1 ), where t ranges over T (S k ).

S k S n t k -1 t 1
We are now able to present our Coq mechanised formal semantics. 2, Figure 3 and Figure 4 where the left part of figures represents SQL Coq 's abstract syntax and the right part the corresponding Coq syntax. We assume that we are given attributes, functions and aggregates. We shall allow strings, integers and booleans to be values, as well as the special NULL. On the top of them, we define usual expressions, first without aggregates e f , and then with aggregates e a . SQL formulae are similar to firstorder formulae except they are always interpreted in a finite domain, which is syntactically refered to as dom in Figure 3. Such formulae will then be used in the context of SQL Alg . SQL Coq sticks, syntactically, as much as possible, to SQL's syntax but the SQL-aware reader shall notice that SQL Coq slightly differs from SQL in different ways. First, for the sake of uniformity, we impose to have the whole select from where group by having construct (no optional where and group by having clauses). When the where clause is empty, it is forced to true. where true group by Group_Fine having true.

A Formal

A further, more subtle, point worth to mention is the distinction we make between e f and e a . Both are expressions but the former are built only with functions (fn) and are evaluated on tuples while the latter also allow unnested6 aggregates (ag) and are, in that case, evaluated on collections of tuples. In the same line, we used the same language for formulae either occurring in the where (dealing with a single tuple) or in the having clause (dealing with collections of tuples) simply by identifying each tuple with its corresponding singleton. Also, no aliases for queries are allowed. This last case is handled by renaming all query's attributes as expressed on last line of Figure 4.

SQL Coq : Semantics

Given a tuple t we note ℓ(t) the attributes occuring in t. We assume that we are given a database instance [[_]] db defined as a function from relation names to bags of tuples 7 as well as predefined, fixed interpretations, [[_]] p , for predicates pr8 , i.e., a function from vectors of values to Booleans, [[_]] a and [[_]] f for aggregates ag and functions fn respectively 9 . As established in Section 2, (complex) expressions occuring in (possibly correlated sub-) queries, are evaluated under a sliced environment, ℰ = [S n ; ...; S 1 ] (or ℰ = (A, G,T ) :: ℰ ′ ), the innermost level, n, corresponding to the first slice. The evaluation of a syntactic entity e of type x in environment ℰ will be denoted by

[[e]] x
ℰ (where x is f for expressions built only with functions, a for expressions built also with aggregates, b for formulae and q for queries). innermost level is chosen (here n), otherwise, the outermost suitable candidate level is chosen as expressed by F e (ℰ , e).

[[c]] f ℰ = c if c is a value [[a]] f [] = default if a is an attribute [[a]] f (A,G,[])::ℰ = [[a]] f ℰ [[a]] f (A,G,t ::T )::ℰ = t .a if a ∈ ℓ(t) [[a]] f (A,G,t ::T )::ℰ = [[a]] f ℰ if a ℓ(t) [[fn(e)]] f ℰ = [[fn]] f ([[e]] f ℰ ) if fn
c ∈ 𝒱 B u (G, c) e ∈ G B u (G, e) e B u (G, e) B u (G, fn(e)) B u ((A ∪ (A ′ ,G,T )∈ℰ G), e)
[[fn(e)]] a ℰ = [[fn]] f ([[e]] a ℰ ) [[ag(e)]] a ℰ = [[ag]] a [[e]] f ((A,G,[t ])::ℰ ′ ) t ∈T iff F e (ℰ , e) = (A, G,T ) :: ℰ ′ Fixpoint (* (B u (G, f )) *) is_built_upon G f := match f with | F_Constant _ ⇒ true | F_Dot _ ⇒ f inS? G | F_Expr s l ⇒ (f ins? G) || forallb (is_built_upon G) l end. Definition (* (S e (l a, env, f )) *) is_a_suitable_env la env f := is_built_upon (map (fun a ⇒ F_Dot a) la ++ flat_map (fun slc ⇒ match slc with (_, G, _) ⇒ G end) env) f. Fixpoint (* (F e (env, f )) *) find_eval_env env f := match env with | nil ⇒ if
Formulae's semantics, given in Figure 7, relies on expressions' semantics. As the syntax is parametrised by a domain dom, similarly formulae's semantics is parametrised by the domain's evaluation. This is expressed, in the Coq development, by Hypothesis I : env_type → dom → bagT., and is expanded as query interpretation, [[_]] q _ , in the formal definition.

Let's finally comment on query semantics, [[_]] q _ , given in Figure 8. For the set theoretic operators, we chose to assign them a bag semantics even if our notations do not explicitely mention all. If one wants to recover the usual set semantics for sq = q 1 op q 2 , one has to apply duplicate elimination thanks to δ (sq) = select * from sq(a i as a i ) a i ∈ℓ(sq) group by ℓ(sq). The most complex case is the select from where group by having one. Informally, a first step consists in evaluating the from and then filtering it thanks to the where formula.

More precisely how to check that a tuple t fullfils where condition w in context ℰ ? According to the definition in Figure 7, w is evaluted w.r.t a single environment. This means that t and ℰ have to be combined into this single environment, ℰ ′ such that [[w]] f ℰ ′ is equal to the evaluation of w, where the attributes a in ℓ(t) are bound to t .a, and the attributes a in S ∈ℰ A(S) are bounded thanks to S ∈ℰ A(T ). This is exactly what is done when ℰ ′ = (ℓ(t), [], [t]) :: ℰ .

Then the (intermediate) collection of tuples obtained is partitioned according to the grouping expressions in the group by G, yielding a collection of collections of tuples: the groups. When there is no grouping clause, the finest partition denoted Group_Fine in the Coq development is used.

The way groups are further filtered w.r.t the having condition h follows the same pattern as where, except that some complex expressions may occur in h. When evaluting an expression of the form ag(e) for a group T , all tuples of the group are needed; when evaluting a simple expression, any tuple of T yields the same result, T being homogeneous w.r.t the grouping criterion G. Hence the proper evaluation environment for filtering the group T w.r.t h in environment ℰ is (ℓ(T ), G,T ) :: ℰ .

Last, the select clause is applied yielding again a collection of tuples as a result. About NULL's At the expression level, NULL's are simply handled by the fact that they behave as an absorbing element w.r.t functions and are simply discarded for aggregates except for count(*) where they contribute as 1. In our formalisation this is expressed as constraints over [[_]] a and [[_]] f . For formulae, we used a 3-valued logic. The evaluation of pr(e) in environment ℰ is equal to unknown iff there exists e i in e such that [[e i ]] a ℰ = NULL. As usual, unknown distributes according to well-known 3-valued logic rules. Quantifiers all and any are respectively seen as a finite conjunct and a finite disjunct in 3-valued logic. Last, e as a in q is evaluated as a finite conjunct of e = t .a where t ranges in [[q]] q , meaning that as soon as e or t .a is evaluated to null, e = t .a is unknown. Eventually, when used into queries' evaluation, the evaluation of formulae yielding unknown results are cast into false. It should be noticed that even if NULL is not equal to nor different from NULL or any other value in the context of formulae, NULL is equal to NULL for grouping. This is taken into account in Figure 8 by a careful definition of partition and of make_groups in the Coq development.

SQL Alg : A Coq Mechanised Algebra for SQL

In this section we relate SQL Coq to relational algebra in order to recover the well-known algebraic equivalences which are exploited by SQL compilers for optimisation purposes.

Relational Algebra in a Nutshell

The (extended) relational algebra, as presented in textbooks [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF], consists of the well-known operators σ (selection), π (projection) and ▷◁ (join) completed with the γ (grouping) together with the set theoretic operators, intersection, union and difference. We focus on the former four operators.

q := r | σ f (q) | π S (q) | q ▷◁ q | γ д,aд (q) In this setting, base relations, r are expressions. The selection operator, allows for filtering collections of tuples according whether they satisfy condition f . The semantics of the operator is

[[σ f (q)]] = {t | t ∈ [[q]] ∧ [[f ]]{x → t }} where [[f ]]{x → t } stands for "t satisfies formula [[f ]]", x being the only free variable of [[f]].
The projection operator has the form π W , and operates on all expressions, q, whose sort contains the subset of attributes W . The semantics of projection is

[[π W (q)]] = {t | W | t ∈ [[q]]}
where the notation t | W represents the tuple obtained from t by keeping only the attributes in W .

The join operator, denoted ▷◁, takes arbitrary expressions q 1 and q 2 whose respective sorts are V and W , and allows to combine tuples from both operands. Its semantics is,

[[q 1 ▷◁ q 2 ]] = {t | ∃v ∈ [[q 1 ]], ∃w ∈ [[q 2 ]], t | V = v ∧ t | W = w }.
Quoting [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF], "operator γ д,aд partitions the tuples of q into groups. Each group consists of all tuples having one particular assignment of values to the grouping attributes in д. If there are no grouping attributes, the entire relation q is one group. For each group, one tuple consisting of the grouping attributes' values for that group and the aggregations, over all tuples of that group, for the aggregated attributes in aд is produced". No further formal definition is given in [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF]. The formal definition corresponding to it is given in Figure 11 where f is instanciated to true for this specific case.

SQL Alg Syntax and Semantics

As presented in [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF], the algebra does not account for having conditions neither for complex expressions (grouping is only possible over attributes and aggregates are computed over single attributes) nor for environments. So as to deal with SQL, ours is much expressive as it allows for grouping over simple expressions and allows complex expressions e a in projections. In order to handle having conditions, that directly operate on groups, SQL Alg extends what is presented in [START_REF] Garcia-Molina | Database systemsthe complete book[END_REF] by adding an extra parameter to γ : the having condition.

Expressions (simple and complex ones) as well as formulae 10 are shared with SQL Coq . In order to define the semantics of SQL Alg 's expressions, environments are needed, for the same reasons as for SQL Coq : accounting for nesting. Hence SQL Alg environments are the same as for SQL Coq . What should be noticed is that ▷◁ is the true natural join, and that γ can be seen as a degenerated case of select from where group by having, where the where condition is absent (or set to true).

Based on our fornmalisation it is possible to define other, derived, operators such as the delta operator (intended to implement the distinct), the semi-join, anti-join and, provided that a null value be defined, the left and full outer-joins as illustrated on Figure 10. Let us at that point formally relate SQL Coq and SQL Alg .

SQL Coq and SQL Alg Are Equivalent

On Figure 12, we give T q (_) a translation from SQL Coq to SQL Alg , and its back translation T Q (_). Both use auxilliary translations (T f (_), resp. T F (_)) which simply traverse formulae in order to translate the queries they contain. Since simple and complex expressions are shared, they are left unchanged by these translations. Notice that in order to translate the Q_empty_tuple construct from the algebra to a SQL query, one has to assume that the database schema contains at least a relation (default_table).

These translations are sound, provided that they are applied on "reasonable" database instances and queries.

W q (tbl)
if tbl is a table

W q (q 1 ) W q (q 2 ) W q (q 1 union q 2 ) W q (q 1 ) W q (q 2 ) W q (q 1 intersect q 2 ) W q (q 1 ) W q (q 2 ) W q (q 1 except q 2 ) disjoint{b i } i i W q (q i ) W f (w) W f (h) W q (selects fromq i (a i asb i )wherew group byG havingh) 10 For algebraic formulae, the domain parameter dom is actually algebraic queries.

W f (f 1 ) W f (f 2 )

W f (f 1 and f 2 )

W f (f 1 ) W f (f 2 ) W f (f 1 or f 2 ) W f (f ) W f (not f ) W f (true) W f (pr(e i ))
W q (q)

W f (exists q)

W q (q)

W f (pr(e i , all q)) W q (q)

W f (pr(e i , any q)) W q (q) e i as a i in q Provided that those conditions be fullfilled we can state the following equivalence Theorem.

ℰ

The proof proceeds by (mutual) structural induction over queries and formulae. Actually the proof is made by induction over the sizes of queries and formulae. It consists of 500 lines of Coq code and heavily relies on a tactic which allows to automate the proofs that size for sub-objects is decreasing. For the correctness of T q (_), the well-formedness hypothesis of the theorem essentially ensures that Cartesian product and natural join coincide. What was interesting is that the well-formedness hypothesis was mandatory and this sheds light on the fact that, indeed, SQL from behaves as a cross product. For both translations, well-sortedness ensures that reasoning over tuples' labels in the evaluation of a query can be made globally, by "statically" computing the labels over a query.

Conclusions

Seeking a formal semantics for SQL has been a longstanding quest for the database community. In this article, we presented a formal, Coq mechanised, executable semantics for a large realistic fragment of SQL.

In an early version of the development, we defined a pure set-theoretic semantics and only addressed the SQL's fragment with no duplicates. Then we addressed the bag aspects of SQL and were pleasantly surprised to discover that adding them was not so problematic. Therefore, the widespread belief that the problem for SQL is to assign it a bag semantics is not as crucial as it seemed to be. Also, grasping NULL's semantics is often considered one of the most difficult aspects to address, this is due to the fact that SQL does not treat them uniformly according to the context. We handled NULL's thanks to a 3-valued logic. What was really challenging was to accurately and faithfully handle correlated sub-queries. Particularly tricky was to grasp SQL's management of expressions and environments in the presence of such queries. The ISO/IEC document was of little help along this path. On the contrary, Coq was an enlightening, very demanding master of invaluable help in defining semantically relevant

  select r.a+2 as b from r; --Q2 select r.a from r where r.a not in (select s.a from s); --Q3 select r.a from r where not exists (select * from s where s.a = r.a); --Q4 select r.a from r except select s.a from s; --Q5 select t.a,count(*) as c from t

Figure 1 .

 1 Figure 1. Semantically Subtle Queries.

Figure 5 .

 5 Figure 5. Simple Expressions' Semantics.

S

  e (A, ℰ , e) c ∈ 𝒱 F e (ℰ , c) = ℰ e 𝒱 F e ([], e) = undefined e 𝒱 F e (ℰ , e) = ℰ ′ F e (((A, G,T ) :: ℰ ), e) = ℰ ′ F e (ℰ , e) = undefined S e (A, ℰ , e) F e (((A, G,T ) :: ℰ ), e) = (A, G,T ) :: ℰ

Figure 6 .

 6 Figure 6. Complex (with Aggregates) Expressions' Semantics.

Theorem 4 . 3 (

 43 SQL Coq ≡ SQL Alg ). Let [[_]] db be a well-sorted database instance and sq be a SQL Coq query, aq a SQL Alg query then:∀ℰ , sq, W q (sq) =⇒ [[T q (sq)]] Q ℰ = [[sq]] q ℰ ∀ℰ , aq, [[T Q (aq)]] q ℰ = [[aq]] Q

  Coq Mechanised Semantics for SQL

SQL Coq addresses the fragment consisting of select [ distinct] from where group by having queries with NULL values, functions, aggregates, quantifiers and nested potentially correlated (in from, where and having clauses) subqueries. It accounts for in, any, all and exists constructs and assigns queries a Coq mechanised (bag) semantics that complies with the Standard. 3.1 SQL Coq : Syntax SQL Coq 's syntax is given on Figure

  Table below, summarises the way the parser handles the different cases for translating the absence or presence of group by into an explicit grouping construct in SQL Coq . corresponds to the finest partition 5 and differs from Group_By [a 1 , . . . , a n ] where [a 1 , . . . , a n ] is the list of labels of the current query. The construct Group_By [a 1 , . . . , a n ] is used in SQL Coq to encode the distinct construct of SQL. Group_By nil corresponds to the coarse partition. We also force explicit and mandatory renaming of attributes, when * is not used. In our syntax, select a, b from t; is expressed by select a as a, b as b from (table t[*])

		SQL		SQL Coq
	aggregate (in select)	group by having
	?	g	?	Group_By g
	✓	✗	?	Group_By nil
	?	✗	✓	Group_By nil
	✗	✗	✗	Group_Fine

Group_Fine

  is a function, and e is a list of simple expressions (* The type of evaluation environnements *) Definition env_type := list (list attribute * group_by * list tuple).

	Fixpoint interp_dot env (a : attribute) :=
	match env with
	| nil ⇒ default_value a
	| (sa, gb, nil) :: env' ⇒ interp_dot env' a
	| (sa, gb, t :: l) :: env' ⇒
	if a inS? labels t then (dot t a) else interp_dot env' a
	end.
	Fixpoint interp_funterm env t :=
	match t with
	| F_Constant c ⇒ c
	| F_Dot a ⇒ interp_dot env a
	| F_Expr f l ⇒
	interp_symb f (List.map (fun x ⇒ interp_funterm env x) l)
	end.

  Definition 4.1. A database instance [[_]] db is well-sorted if and only if all tuples in the same table have the same labels:∀r, t 1 , t 2 , t 1 ∈ [[r ]] db ∧ t 2 ∈ [[r ]] db =⇒ ℓ(t 1 ) = ℓ(t 2 ).Definition 4.2. A SQL Coq query sq is well-formed if and only if all labels in its from clauses are pairwise disjoint and its sub-queries are well-formed:

If this subquery is a select from ... these are the names in the select.

When there is a grouping clause at this level, it is an homogeneous group, otherwise it is a single tuple.

Those appearing in the group by clause of the level ; when there are no such grouping expressions, all attributes of the level are allowed.

The partition consisting of the collection of singletons, one singleton for each tuple.

e a is of the form: avg(a); sum(a+b); sum(a+b)+3; sum(a+b)+avg( c+3) but not of avg(sum(c)+a)

These multisets enjoy some list-like operators such as empty, map, filter, etc.

pr is <, in etc.

* Work funded by the DataCert ANR project: ANR-15-CE39-0009.

The semantics of simple expressions, which poses no difficulties, is given in Figure 5. The semantics of complex expressions detailed in Figure 6, deserves comments. When the complex expression is headed by a function, fn(e), it simply amounts to a recursive call. When the complex expression is of the form ag(e), according to Section 2, one has first to find the suitable level of nesting for getting the group to be split into. Then, produce the list of values by evaluating e, and then compute the evaluation of ag against this list of values. In environment ℰ =[S n ; . . . S 1 ], level i is a suitable candidate expressed by S e (A(S i ), [S i-1 ; . . . ; S 1 ], e) on Figure 6 whenever e is built upon G = A(S i ) ∪ j <i G(S j ) which is in turn expressed by B u (G, e) on Figure 6. When e is a constant, the Conference'17, July 2017, Washington, DC, USA

γ (e a as attribute, e f ,formula) (Q)

queries. Such a set of queries, augmented with others not listed in this article, could serve as a benchmark for testing SQL's other implementations. Thanks to our formal semantics we have been able to relate SQL Coq and SQL Alg establishing, the first, to our best knowledge, equivalence result for that SQL fragment. Moreover, by doing so, we recover the well-known algebraic equivalences presented in textbooks upon which are based most of optimisations used in practice. Such equivalences were proven, using Coq, in [START_REF] Benzaken | A Coq Formalization of the Relational Data Model[END_REF]. Even if we knew it, it confirmed us that, SQL having initially been designed as a domain specific language intended not to be Turing-complete, the fact of adding more features along the time in the standardisation process, seriously, and sadly, departed it from its original elegant foundations. By formally relating SQL and an extended relational algebra, we, humbly, also wanted to pay tribute to the pionneers that designed the foundational aspects of RDBMS's.

Our long term goal is to provide a Coq verified compiler for SQL. The work presented in this article allows to obtain a certified semantic analyser that we plan to extend to features like order by. In [START_REF] Benzaken | A Coq formalisation of SQL's execution engines[END_REF] we provided a certification of the physical layer of a SQL engine where mainstream physical operators such as sequential scans, nested loop joins,