research-article

Open access

Generating collection transformations from proofs

Authors:

Michael Benedikt,

Pierre PradicAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 14, Pages 1 - 28

https://doi.org/10.1145/3434295

Published: 04 January 2021 Publication History

Abstract

Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets.

In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig's interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them.

We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it.

References

[1]

Serge Abiteboul and Catriel Beeri. 1995. The Power of Languages for the Manipulation of Complex Values. VLDB J. 4, 4 ( 1995 ), 727-794.

Digital Library

[2]

Serge Abiteboul and Nicole Bidoit. 1986. Non First Normal Form Relations: An Algebra Allowing Data Restructuring. J. Comput. Syst. Sci. 33, 3 ( 1986 ), 361-393.

Digital Library

[3]

Foto Afrati and Rada Chirkova. 2019. Answering Queries Using Views. Morgan & Claypool Publishers.

[4]

H. Andréka, J. X. Madarász, and I. Németi. 2008. Definability of New Universes in Many-sorted logic. ( 2008 ). manuscript available at old.renyi.hu/pub/algebraic-logic/kurzus10/amn-defi.pdf.

[5]

Michael Benedikt, Balden Ten Cate, Julien Leblay, and Efthymia Tsamoura. 2016. Generating plans from proofs: the interpolation-based approach to query reformulation. Morgan Claypool.

[6]

Michael Benedikt and Christoph Koch. 2009. From XQuery to Relational Logics. ACM TODS 34, 4 ( 2009 ), 25 : 1-25 : 48.

[7]

E. W. Beth. 1953. On Padoa's Method in the Theory of Definitions. Indagationes Mathematicae 15 ( 1953 ), 330-339.

[8]

Mikolaj Bojanczyk, Laure Daviaud, and Shankara Narayanan Krishna. 2018. Regular and First-Order List Functions. In LICS.

[9]

Peter Buneman, Shamim A. Naqvi, Val Tannen, and Limsoon Wong. 1995. Principles of Programming with Complex Objects and Collection Types. Theor. Comput. Sci. 149, 1 ( 1995 ), 3-48.

[10]

James Cheney, Sam Lindley, and Philip Wadler. 2014. Query shredding: eficient relational evaluation of queries over nested multisets. In SIGMOD.

[11]

Thomas Colcombet and Christof Löding. 2007. Transforming structures by set interpretations. Logical Methods in Computer Science 3, 2 ( 2007 ).

[12]

Ezra Cooper. 2009. The Script-Writer's Dream: How to Write Great SQL in Your Own Language, and Be Sure It Will Succeed. In DBPL.

[13]

Coq. 2020. The Coq Proof Assistant. ( 2020 ). coq.inria.fr.

[14]

William Craig. 1957. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. Journal of Symbolic Logic 22, 3 ( 1957 ), 269-285.

[15]

Melvin Fitting. 1996. First-order Logic and Automated Theorem Proving. Springer.

[16]

R. O. Gandy. 1974. Set-theoretic functions for elementary syntax. In Proceedings of Symposia in Pure Mathematics, 13, Part II, Thomas Jech (Ed.). American Mathematical Society, 103-126.

[17]

Jeremy Gibbons. 2016. Comprehending Ringads-For Phil Wadler, on the Occasion of his 60th Birthday. In A List of Successes That Can Change the World-Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday.

[18]

Jeremy Gibbons, Fritz Henglein, Ralf Hinze, and Nicolas Wu. 2018. Relational algebra by way of adjunctions. PACMPL 2, ICFP ( 2018 ).

[19]

Torsten Grust, Jan Rittinger, and Tom Schreiber. 2010. Avalanche-Safe LINQ Compilation. PVLDB 3, 1-2 ( 2010 ), 162--172.

Digital Library

[20]

Alon Y. Halevy. 2001. Answering queries using views: A survey. VLDB Journal 10, 4 ( 2001 ), 270-294.

Digital Library

[21]

Kryštof Hoder, Laura Kovács, and Andrei Voronkov. 2010. Interpolation and Symbol Elimination in Vampire.

[22]

Wilfrid Hodges. 1993. Model Theory. Cambridge University Press.

[23]

Wilfrid Hodges, I.M. Hodkinson, and Dugald Macpherson. 1990. Omega-categoricity, relative categoricity and coordinatisation. Annals of Pure and Applied Logic 46, 2 ( 1990 ), 169-199.

[24]

Qinheping Hu and Loris D'Antoni. 2017. Automatic Program Inversion Using Symbolic Transducers. In PLDI.

[25]

Bart Jacobs. 2001. Categorical Logic and Type Theory. Elsevier.

[26]

R. B. Jensen. 1972. The fine structure of the constructible hierarchy, with a section by Jack Silver. Annals of Mathematical Logic 4 ( 1972 ), 229-308.

[27]

Christoph Koch. 2006. On the Complexity of Non-recursive XQuery and Functional Query Languages on Complex Values. ACM TODS 31, 4 ( 2006 ), 1215-1256.

[28]

Christoph Koch, Daniel Lupei, and Val Tannen. 2016. Incremental View Maintenance For Collection Programming. In PODS.

[29]

Phokion G. Kolaitis. 1990. Implicit Definability on Finite Structures and Unambiguous Computations. In LICS.

[30]

Maurizio Lenzerini. 2002. Data Integration: A Theoretical Perspective. In PODS.

Digital Library

[31]

M. Makkai. 1964. On a generalization of a theorem of E. W. Beth. Acta Mathematica Academiae Scientiarum Hungaricae 15 ( 1964 ), 227-235.

[32]

K.L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In CAV.

[33]

Erik Meijer, Brian Beckman, and Gavin Bierman. 2006. LINQ: Reconciling Object, Relations and XML in the. NET Framework. In SIGMOD.

Digital Library

[34]

Sergey Melnik, Andrey Gubarev, Jing Jing Long, Geofrey Romer, Shiva Shivakumar, Matt Tolton, and Theo Vassilakis. 2010. Dremel: Interactive Analysis of Web-Scale Datasets. PVLDB 3, 1-2 ( 2010 ), 330-339.

Digital Library

[35]

Andrzej Mostowski. 1949. An undecidable arithmetical statement. Fundamenta Mathematicae 36, 1 ( 1949 ), 143-164.

[36]

Alan Nash, Luc Segoufin, and Victor Vianu. 2010. Views and queries: Determinacy and rewriting. ACM TODS 35, 3 ( 2010 ).

[37]

Martin Otto. 2000. An interpolation theorem. Bulletin of Symbolic Logic 6, 4 ( 2000 ), 447-462.

[38]

Jan Paredaens and Dirk Van Gucht. 1992. Converting Nested Algebra Expressions into Flat Algebra Expressions. ACM TODS 17, 1 ( 1992 ), 65-93.

[39]

Vladimir Yu. Sazonov. 1985. Collection principle and existential quantifier. Vychislitel'nye sistemy 107 ( 1985 ), 30-39.

[40]

Luc Segoufin and Victor Vianu. 2005. Views and queries: determinacy and rewriting. In PODS.

[41]

Saurabh Srivastava, Sumit Gulwani, Swarat Chaudhuri, and Jefrey S. Foster. 2011. Path-Based Inductive Synthesis for Program Inversion. In PLDI.

[42]

Dan Suciu. 1995. Parallel Programming Languages for Collections. Ph.D. Dissertation. Univ. Pennsylvania.

[43]

David Toman and Grant Weddell. 2011. Fundamentals of Physical Design and Query Compilation. Morgan Claypool.

[44]

Alexander Ulrich. 2019. Query Flattening and the Nested Data Parallelism Paradigm. Ph.D. Dissertation. University of Tübingen, Germany. https://publikationen.uni-tuebingen.de/xmlui/handle/10900/87698/

[45]

Jan Van den Bussche. 2001. Simulation of the Nested Relational Algebra by the Flat Relational Algebra, with an Application to the Complexity of Evaluating Powerset Algebra Expressions. Theoretical Computer Science 254, 1-2 ( 2001 ), 363-377.

[46]

Limsoon Wong. 1994. Querying Nested Collections. Ph.D. Dissertation. Univ. Pennsylvania.

[47]

Limsoon Wong. 1996. Normal Forms and Conservative Extension Properties for Query Languages over Collection Types. J. Comput. Syst. Sci. 52, 3 ( 1996 ), 495-505.

Digital Library

Cited By

Benedikt MPradic CWernhard CGeerts FNgo HSintos S(2023)Synthesizing Nested Relational Queries from Implicit SpecificationsProceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3584372.3588653(33-45)Online publication date: 18-Jun-2023
https://doi.org/10.1145/3584372.3588653
Ricciotti WCheney J(2021)Query LiftingProgramming Languages and Systems10.1007/978-3-030-72019-3_21(579-606)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_21

Index Terms

Generating collection transformations from proofs
1. Theory of computation
  1. Logic
    1. Proof theory
  2. Theory and algorithms for application domains
    1. Database theory
      1. Logic and databases

Recommendations

On the naturalness of proofs
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Proofs play a key role in reasoning about programs and verification of properties of systems. Mechanized proof assistants help users in developing and checking the consistency of proofs using the proof language developed by the systems; but even then ...
On inductive and coinductive proofs via unfold/fold transformations
LOPSTR'09: Proceedings of the 19th international conference on Logic-Based Program Synthesis and Transformation

We consider a new application condition of negative unfolding, which guarantees its safe use in unfold/fold transformation of stratified logic programs. The new condition of negative unfolding is a natural one, since it is considered as a special case ...
Reprint of

In this paper it is suggested to generalize our understanding of general (structural) proof theory and to consider it as a general theory of two kinds of derivations, namely proofs and dual proofs. The proposal is substantiated by (i) considerations on ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

UK Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
535
Total Downloads

Downloads (Last 12 months)100
Downloads (Last 6 weeks)21

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Benedikt MPradic CWernhard CGeerts FNgo HSintos S(2023)Synthesizing Nested Relational Queries from Implicit SpecificationsProceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3584372.3588653(33-45)Online publication date: 18-Jun-2023
https://doi.org/10.1145/3584372.3588653
Ricciotti WCheney J(2021)Query LiftingProgramming Languages and Systems10.1007/978-3-030-72019-3_21(579-606)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_21

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents