On principal types of combinators

摘要

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- and in the lambda g-calculus, while the two problems become equivalent for the BCK-lambda- 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 a-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. (C) 2000 Elsevier Science B.V. All rights reserved. [References: 13]