License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.28
URN: urn:nbn:de:0030-drops-123506
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12350/
Go to the corresponding LIPIcs Volume Portal

Ricciotti, Wilmer ; Cheney, James

Strongly Normalizing Higher-Order Relational Queries

pdf-format:
LIPIcs-FSCD-2020-28.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{ricciotti_et_al:LIPIcs:2020:12350,
  author =	{Wilmer Ricciotti and James Cheney},
  title =	{{Strongly Normalizing Higher-Order Relational Queries}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{28:1--28:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12350},
  URN =		{urn:nbn:de:0030-drops-123506},
  doi =		{10.4230/LIPIcs.FSCD.2020.28},
  annote =	{Keywords: Strong normalization, ⊤⊤-lifting, Nested relational calculus, Language-integrated query}
}

Keywords: Strong normalization, ⊤⊤-lifting, Nested relational calculus, Language-integrated query
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI