On principal types of combinators

Sabine Broda and Luís Damas

TCS (to appear)


In this paper we study (in some cases) the relationship between the combinatory completeness of a set of typable combinators, with simple types, for a system of lambda calculus and the axiomatic completeness, under substitution and modus ponens, of the respective set of principal types for the corresponding logical system. We show that combinatory completeness is a necessary, but not sufficient, condition for axiomatic completeness in the lambda-K-calculus and in the lambda-I-calculus, while the two problems become equivalent for the BCK-lambda-calculus as well as for the BCI-lambda-calculus. Furthermore, we present an algorithm which, whenever (B,alpha) is a principal pair for some normal BCK-lambda-term M, reconstructs M up to alpha-conversion and which fails if there is no normal BCK-lambda-term for which (B,alpha) is a principal pair. From the correctness proof of the algorithm we also obtain another proof for the fact that each BCK-lambda-term in normal form is completely determined by its principal pairs.