###
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

#### Abstract

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.