Wilmer Ricciotti ; James Cheney - Strongly-Normalizing Higher-Order Relational Queries

lmcs:6940 - Logical Methods in Computer Science, August 17, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:23)2022
Strongly-Normalizing Higher-Order Relational Queries

Authors: Wilmer Ricciotti ; James Cheney

    Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about the nested relational calculus, stating that its queries can be algorithmically translated to SQL, as long as their result type is a flat relation. Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However, the translation of higher-order relational queries to SQL relies on a rewrite system for which no strong normalization proof has been published: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the $\top\top$-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also show how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.


    Volume: Volume 18, Issue 3
    Published on: August 17, 2022
    Accepted on: June 21, 2022
    Submitted on: December 1, 2020
    Keywords: Computer Science - Programming Languages,03B38 (Primary), 68N15 (Secondary)
    Fundings :
      Source : OpenAIRE Research Graph
    • A programming language bridging theory and practice for scientific data curation; Funder: European Commission; Code: 682315

    Share

    Consultation statistics

    This page has been seen 623 times.
    This article's PDF has been downloaded 321 times.