| Autor: |
Wilmer Ricciotti, James Cheney |
| Jazyk: |
angličtina |
| Rok vydání: |
2022 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Vol Volume 18, Issue 3 (2022) |
| Druh dokumentu: |
article |
| ISSN: |
1860-5974 |
| DOI: |
10.46298/lmcs-18(3:23)2022 |
| Popis: |
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. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
