Strongly Normalizing Higher-Order Relational Queries

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish
Title of host publication5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
EditorsZena Ariola
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages22
ISBN (Print)978-3-95977-155-9
Publication statusPublished - 28 Jun 2020
Event5th International Conference on Formal Structures for Computation and Deduction - Paris, France
Duration: 29 Jun 20206 Jul 2020

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


Conference5th International Conference on Formal Structures for Computation and Deduction
Abbreviated titleFSCD 2020
Internet address


  • Strong normalization
  • ⊤⊤-lifting
  • nested relational calculus
  • Language-integrated query


Dive into the research topics of 'Strongly Normalizing Higher-Order Relational Queries'. Together they form a unique fingerprint.

Cite this