ACM SIGMOD Anthology ACM SIGMOD dblp.uni-trier.de

Functional Database Query Languages as Typed Lambda Calculi of Fixed Order.

Gerd G. Hillebrand, Paris C. Kanellakis: Functional Database Query Languages as Typed Lambda Calculi of Fixed Order. PODS 1994: 222-231
@inproceedings{DBLP:conf/pods/HillebrandK94,
  author    = {Gerd G. Hillebrand and
               Paris C. Kanellakis},
  title     = {Functional Database Query Languages as Typed Lambda Calculi of
               Fixed Order},
  booktitle = {Proceedings of the Thirteenth ACM SIGACT-SIGMOD-SIGART Symposium
               on Principles of Database Systems, May 24-26, 1994, Minneapolis,
               Minnesota},
  publisher = {ACM Press},
  year      = {1994},
  isbn      = {0-89791-642-5},
  pages     = {222-231},
  ee        = {http://doi.acm.org/10.1145/182591.182615, db/conf/pods/pods94-222.html},
  crossref  = {DBLP:conf/pods/94},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
BibTeX

Abstract

We present a functional framework for database query languages, which is analogous to the conventional logical framework of first-order and fixpoint formulas over finite structures. We use atomic constants of order 0, equality among these constants, variables, application, lambda abstraction, and Let-abstraction; all typed using fixed order less or equal to 5 functionalities. In this framework, proposed in [21] for arbitrary order functionalities, queries and databases are both typed lambda terms, evaluation is by reduction, and the main programming technique is list iteration. We define two families of languages: TLI(=,i) or simply-typed list iteration of order i+3 with equality, and MLI(=,i) or ML-typed list iteration of order i+3 with equality; we use i+3 since our list representation of databases requires at least order 3. We show that: FO-queries isa-subset-of TLI(=,0) isa-subset-of MLI(=,0) isa-subset-of LOGSPACE-queries isa-subset-of TLI(=,1) equals MLI(=,1) equals PTIME-queries isa-subset-of TLI(2), where equality is no longer a primitive in TLI(2). We also show that ML type inference, restricted to fixed order, is polynomial in the size of the program typed. Since programming by using low order functionalities and type inference is common in functional languages, our results indicate that such programs suffice for expressing efficient computations and that their ML-types can be efficiently inferred.

Copyright © 1994 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.


Load The ACM SIGMOD Anthology, CDROM Edition, Volume 1-3, PODS '82-'98. and ... Load The ACM SIGMOD Anthology, Silver Edition, DVD 1, Proceedings. and ... BibTeX

Printed Edition

Proceedings of the Thirteenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, May 24-26, 1994, Minneapolis, Minnesota. ACM Press 1994, ISBN 0-89791-642-5
Contents BibTeX

Online Edition: ACM Digital Library

[Abstract and Index Terms]
[Full Text in PDF Format, 1035 KB]

References

[1]
Serge Abiteboul, Catriel Beeri: The Power of Languages for the Manipulation of Complex Values. VLDB J. 4(4): 727-794(1995) BibTeX
[2]
Serge Abiteboul, Catriel Beeri, Marc Gyssens, Dirk Van Gucht: An Introduction to the Completeness of Languages for Complex Objects and Nested Relations. NF² 1987: 117-138 BibTeX
[3]
Serge Abiteboul, Paris C. Kanellakis: Database Theory Column: Query Languages for Complex Object Databases. SIGACT News 21(3): 9-18(1990) BibTeX
[4]
Serge Abiteboul, Victor Vianu: Datalog Extensions for Database Queries and Updates. J. Comput. Syst. Sci. 43(1): 62-124(1991) BibTeX
[5]
Serge Abiteboul, Victor Vianu: Generic Computation and Its Complexity. STOC 1991: 209-219 BibTeX
[6]
...
[7]
Stephen Bellantoni, Stephen A. Cook: A New Recursion-Theoretic Characterization of the Polytime Functions (Extended Abstract). STOC 1992: 283-293 BibTeX
[8]
Val Tannen, Peter Buneman, Shamim A. Naqvi: Structural Recursion as a Query Language. DBPL 1991: 9-19 BibTeX
[9]
Val Tannen, Peter Buneman, Limsoon Wong: Naturally Embedded Query Languages. ICDT 1992: 140-154 BibTeX
[10]
Val Tannen, Ramesh Subrahmanyam: Logical and Computational Aspects of Programming with Sets/Bags/Lists. ICALP 1991: 60-75 BibTeX
[11]
Peter Buneman, Robert E. Frankel, Rishiyur S. Nikhil: An Implementation Technique for Database Query Languages. ACM Trans. Database Syst. 7(2): 164-186(1982) BibTeX
[12]
Ashok K. Chandra, David Harel: Computable Queries for Relational Data Bases. J. Comput. Syst. Sci. 21(2): 156-178(1980) BibTeX
[13]
Ashok K. Chandra, David Harel: Structure and Complexity of Relational Queries. J. Comput. Syst. Sci. 25(1): 99-128(1982) BibTeX
[14]
Ashok K. Chandra, David Harel: Horn Clauses Queries and Generalizations. J. Log. Program. 2(1): 1-15(1985) BibTeX
[15]
...
[16]
...
[17]
...
[18]
...
[19]
Steven Fortune, Daniel Leivant, Michael O'Donnell: The Expressiveness of Simple and Second-Order Type Structures. J. ACM 30(1): 151-185(1983) BibTeX
[20]
Yuri Gurevich: Algebras of Feasible Functions. FOCS 1983: 210-214 BibTeX
[21]
Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson: Database Query Languages Embedded in the Typed Lambda Calculus. LICS 1993: 332-343 BibTeX
[22]
Richard Hull, Jianwen Su: On the Expressive Power of Database Queries with Intermediate Types. J. Comput. Syst. Sci. 43(1): 219-267(1991) BibTeX
[23]
Neil Immerman: Relational Queries Computable in Polynomial Time. Information and Control 68(1-3): 86-104(1986) BibTeX
[24]
Neil Immerman: Languages that Capture Complexity Classes. SIAM J. Comput. 16(4): 760-778(1987) BibTeX
[25]
Neil Immerman, Sushant Patnaik, David W. Stemple: The Expressiveness of a Family of Finite Set Languages. PODS 1991: 37-52 BibTeX
[26]
...
[27]
A. J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn: ML Typability is DEXTIME-Complete. CAAP 1990: 206-220 BibTeX
[28]
A. J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn: The Hierarchy of Finitely Typed Functional Programs (Short Version). LICS 1987: 225-235 BibTeX
[29]
Phokion G. Kolaitis, Christos H. Papadimitriou: Why not Negation by Fixpoint? J. Comput. Syst. Sci. 43(1): 125-144(1991) BibTeX
[30]
Gabriel M. Kuper, Moshe Y. Vardi: On the Complexity of Queries in the Logical Data Model. Theor. Comput. Sci. 116(1&2): 33-57(1993) BibTeX
[31]
Daniel Leivant, Jean-Yves Marion: Lambda Calculus Characterizations of Poly-Time. Fundam. Inform. 19(1/2): 167-184(1993) BibTeX
[32]
...
[33]
Harry G. Mairson: A Simple Proof of a Theorem of Statman. Theor. Comput. Sci. 103(2): 387-394(1992) BibTeX
[34]
Robin Milner: A Theory of Type Polymorphism in Programming. J. Comput. Syst. Sci. 17(3): 348-375(1978) BibTeX
[35]
...
[36]
...
[37]
Richard Statman: The Typed lambda-Calculus is not Elementary Recursive. Theor. Comput. Sci. 9: 73-81(1979) BibTeX
[38]
Moshe Y. Vardi: The Complexity of Relational Query Languages (Extended Abstract). STOC 1982: 137-146 BibTeX
[39]
Limsoon Wong: Normal Forms and Conservative Properties for Query Languages over Collection Types. PODS 1993: 26-36 BibTeX

Referenced by

  1. Serge Abiteboul, Gabriel M. Kuper, Harry G. Mairson, Alexander A. Shvartsman, Moshe Y. Vardi: In Memoriam Paris C. Kanellakis. ACM Comput. Surv. 28(1): 3-15(1996)
  2. Catriel Beeri, Tova Milo, Paula Ta-Shma: On Genericity and Parametricity. PODS 1996: 104-116
  3. Serge Abiteboul, Gerd G. Hillebrand: Space Usage in Functional Query Languages. ICDT 1995: 439-454
  4. Val Tannen: Tutorial: Languages for Collection Types. PODS 1994: 150-154
BibTeX
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (info@acm.org), Corrections: anthology@acm.org
DBLP: Copyright © by Michael Ley (ley@uni-trier.de), last change: Sat May 16 23:34:11 2009