The paper presents the connection between λ-calculus and cartesian closed categories both in an untyped and purely syntactic setting. More specifically we establish a syntactic equivalence theorem between what we call categorical combinatory logic and λ-calculus with explicit products and projections, with β and þ-rules as well as with surjective pairing. “Combinatory logic“ is of course inspired by Curry's combinatory logic, based on the well known S,K,I. Compiling λ-calculus happens to be natural and provokes only n log n code expansion (which is achieved only with infinitely many S,K-like combinators). Moreover categorical combinatory logic is entirely faithful to β-reduction where combinatory logic needs additional rather complex and unnatural axioms to be. The paper is intended as a mathematical foundation for developing implementations of functional programming languages based on a “categorical abstract machine”, as developed in forthcoming papers.