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.