A Coq certified translation from an extension of relational algebra for SQL to a nested algebra
Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée
Résumé
In 1974, Boyce and Chamberlin created sql using the concepts of the relational algebra proposed by Codd in 1970, but as it evolved, its formal semantics became more and more complex. The small fragment select from where of SQL can be mapped to a relational algebra, with bag's semantics and by restricting expressions and formulae to those which can be expressed in relational algebra. To capture the semantics of the much more realistic fragment select from where group by having, taking into account all the expressions including those with aggregates, all forms of formulas, null values and, even more subtle, the specific SQL's environments, Benzaken and Contejean propose SQLalg which is an extension of relational algebra with a new operator for the group by having part designed specifically to take into account all the aspects of SQL cited above. Can this same fragment of SQL, with all its subtleties, be captured by nested relational algebra ? The present work formally proves that the answer to this question is yes. Indeed, we have built a certified translation, formalized in Coq, from SQLalg to NRAᵉ, which is a formalization in Coq of the nested relational algebra. The translation supports simple and complex expressions, SQL's formulae and perfectly reflects how environments are built and manipulated, especially for aggregates and for correlated queries. This work is part of a more global framework : the DBCert project which is a compilation chain certified in Coq from SQL to JavaScript.
En 1974, Boyce et Chamberlin ont créé le langage SQL en se basant sur l'algèbre relationnelle proposée par Codd en 1970, mais à mesure d'extensions, la sémantique formelle de SQL s'est éloignée de celle de l'algèbre relationnelle. Le petit fragment select from where de SQL peut correspondre à une algèbre relationnelle avec une sémantique multiensemble en restreignant les expressions et les formules à celles exprimables en algèbre relationnelle. Pour capturer la sémantique du fragment beaucoup plus réaliste select from where group by having en prenant en compte toutes les expressions y compris celles avec agrégats, toutes les formes de formules, les valeurs nulles et, encore plus subtil, les environnements très particuliers de SQL, Benzaken et Contejean ont proposé l'algèbre SQLalg qui est une extension de l'algèbre relationnelle avec un nouvel opérateur pour la partie group by having conçu spécifiquement pour prendre en compte tous les aspects de SQL cités précédemment. Ce même fragment de SQL, avec toute ses subtilités, est-il capturable par l'algèbre relationnelle imbriquée ? Cette thèse prouve formellement que oui. En effet, nous proposons une traduction, certifiée en coq, de SQLalg vers NRAᵉ, qui est une formalisation en coq de l'algèbre relationnelle imbriquée. La traduction prend en compte les expressions simples et complexes, les formules SQL et reflète parfaitement comment les environnements sont construits et manipulés, spécialement pour les agrégats et les requêtes corrélées. Ce travail s'inscrit dans un cadre plus global, celui du projet DBCert: une chaîne de compilation certifiée en Coq de SQL vers JavaScript.
Origine : Version validée par le jury (STAR)