Database Query Languages Embedded in the Typed Lambda Calculus

We investigate the expressive power of the typedλ-calculus when expressing computations over finite structures, i. e. , databases. We show that the simply typedλ-calculus can express various database query languages such as the relational algebra, fixpoint logic, and the complex object algebra. In our embeddings, inputs and outputs areλ-terms encoding databases, and a program expressing a query is aλ-term which types when applied to an input and reduces to an output. Our embeddings have the additional property that PTIME computable queries are expressible by programs that, when applied to an input, reduce to an output in a PTIME sequence of reduction steps. Under our database input-output conventions, all elementary queries are expressible in the typedλ-calculus and the PTIME queries are expressible in the order-5 (order-4) fragment of the typedλ-calculus (with equality).

Authors

• Gerd G. Hillebrand
• Paris C. Kanellakis
• Harry G. Mairson

Keywords

No keywords are indexed for this paper.