Projects per year
Abstract
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 monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and 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 there is no published proof of the central strong normalization property for higher-order nested relational queries: 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 ⊤⊤-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also sketch how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.
Original language | English |
---|---|
Title of host publication | 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) |
Editors | Zena Ariola |
Publisher | Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany |
Pages | 1-22 |
Number of pages | 22 |
ISBN (Print) | 978-3-95977-155-9 |
DOIs | |
Publication status | Published - 28 Jun 2020 |
Event | 5th International Conference on Formal Structures for Computation and Deduction - Paris, France Duration: 29 Jun 2020 → 6 Jul 2020 https://fscd2020.org/ |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Publisher | Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik |
Volume | 167 |
ISSN (Print) | 1868-8969 |
Conference
Conference | 5th International Conference on Formal Structures for Computation and Deduction |
---|---|
Abbreviated title | FSCD 2020 |
Country/Territory | France |
City | Paris |
Period | 29/06/20 → 6/07/20 |
Internet address |
Keywords
- Strong normalization
- ⊤⊤-lifting
- nested relational calculus
- Language-integrated query
Fingerprint
Dive into the research topics of 'Strongly Normalizing Higher-Order Relational Queries'. Together they form a unique fingerprint.-
Skye-A programming language bridging theory and practice for scientific data curation
1/09/16 → 31/08/22
Project: Research
-