On Principal Types of BCK-lambda-terms

Sabine Broda and Luís Damas

Wollic 2007


Abstract

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 obtain a characterization of the complete set of principal types of BCK-lambda-terms.