On Principal Types of BCK-lambda-terms
Sabine Broda and Luís Damas
Condensed BCK-logic, i.e. the set of BCK-theorems provable
by the condensed detachment rule of Carew Meredith, has been shown to
be exactly the set of principal types of BCK-lambda-terms. In 1993
Sachio Hirokawa gave a characterization of the set of principal types
of BCK-lambda-terms in beta-normal form based on
a relevance relation that he defined between the type variables in a type.
We define a symmetric notion of this and call it dependence relation.
Then, using the notion of beta-S-reduction introduced by de Groote, we
characterization of the complete set of principal types of