Tech Report CS-94-24

Finite Model Theory in the Simply Typed Lambda Calculus

Gerd G. Hillebrand

May 1994


Church's simply typed lambda-calculus is a very basic framework for functional programming language research. However, it is common to augment this framework with additional programming constructs, because its expressive power for functions over the domain of Church numerals is very limited. In this thesis: (1)~We re-examine the expressive power of the ``pure'' simply typed lambda-calculus, but over encodings of finite relational structures, i.~e., {\em finite models} or {\em databases}. In this novel framework the simply typed lambda-calculus expresses all elementary functions from finite models to finite models. In addition, many common database query languages, e.~g., relational algebra, Datalog with negation, and the Abiteboul/Beeri complex object algebra, can be embedded into it. The embeddings are feasible in the sense that the lambda-terms corresponding to PTIME queries can be evaluated in polynomial time. (2)~We examine fixed-order fragments of the simply typed lambda-calculus to determine machine independent characterizations of complexity classes. For this we augment the calculus with atomic constants and equality among atomic constants. We show that over ordered structures, the order~3, 4, 5, and~6 fragments express exactly the first-order, PTIME, PSPACE, and EXPTIME queries, respectively, and we conjecture that for general $k\ge1$, order~$2k+4$ expresses exactly the $k$-EXPTIME queries and order~$2k+5$ expresses exactly the $k$-EXPSPACE queries. (3)~We also re-examine other functional characterizations of PTIME and we show that {\em method schemas with ordered objects} express exactly PTIME. This is a first-order framework proposed for object-oriented databases---as opposed to the above higher-order frameworks. In summary, this research provides a link between finite model theory (and thus computational complexity), database theory, and programming language theory. It sheds new light on the expressive power of the simply typed lambda-calculus. It transforms classical complexity questions into questions of expressibility. Finally, it provides new examples of pure functional database query languages.

(complete text in pdf or gzipped postscript)