What is a universal higher-order programming language?

Abstract

Classic recursion theory asserts that all conventional programming languages are equally expressive because they can define all partial recursive functions over the natural numbers. This statement is misleading because programming languages support and enforce a more abstract view of data than bitstrings. In particular, most real programming languages support some form of higher-order data such as potentially infinite streams (input and output), lazy trees, and functions. In this paper, we develop a theory of higher-order computability suitable for comparing the expressiveness of sequential, deterministic programming languages. The theory is based on the construction of a new universal domain T-and corresponding universal language KL. The domain T is universal for “sequential” domains; KL can define all the computable elements of T, including the elements corresponding to computable sequential functions. In addition, T-preserves maximality of finite elements in embeddings, so the termination behavior of programs is preserved by embeddings in T.