Technical Report: DCC-97-4

On Principal Types of Stratified Combinators

Sabine Broda e Luis Damas

Departamento de Ciência de Computadores & LIACC
Faculdade de Ciências, Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal

April 1997


In this paper we study (in some cases) the relationship between the combinatory completeness of a set of stratified combinators 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-I-calculus, while the two problems become equivalent for the BCK-lambda- as well as for the BCI-lambda-calculus. Furthermore, we present another proof for the fact that each BCK-lambda-term in normal form is completely determined by its principal pairs.

Keywords: Lambda Calculus, Combinatory Completeness, Propositional Calculi.