Database Query Languages Embedded in the Typed Lambda Calculus

Abstract

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). © 1996 Academic Press, Inc.