A category-theoretic characterization of functional completeness

AbstractFunctional languages are based on the notion of application: programs may be applied to data or programs. By application one may define algebraic functions; and a programming language is functionally complete when any algebraic function f(x1,…,xn) is representable (i.e. there is a constant a such that f(x1,…,xn) = (a·x1,…,xn). Combinatory logic is the simplest type-free language which is functionally complete. In a sound category-theoretic framework the constant a may be considered as an “abstract Gödel-number” for f, when Gödel-numberings are generalized to “principal morphisms”, in suitable categories. By this, models of combinatory logic are categorically characterized and their relation is given to lambda-calculus models within cartesian closed categories. Finally, the partial recursive functionals in any finite higher type are shown to yield models of combinatory logic