Tech Report CS-93-06

Database Query Languages Embedded in the Typed Lambda Calculus

Gerd G. Hillebrand, Paris C. Kanellakis and Harry G. Mairson

Revised December 1995


We show how to "naturally embed" in the typed lambda-calculus with equality many database query languages, including the relational calculus/algebra, inflationary Datalog with negation, and the complex object calculus/algebra. We consider embeddings such that a database is a lambda-term coding a list of tuples and a query is a lambda-term which when applied to the input database normalizes to the output database. In addition, if the query expressed is a PTIME query then the normal form can be computed in a number of reduction steps polynomial in the size of the input database. We also show that, for all PTIME queries, there is such an embedding in the order-3 typed lambda-calculus with equality.

(complete text in pdf or gzipped postscript)