BCK-combinators and linear \(\lambda\)-terms have types (Q1119620)

The main theorem of this paper proves that every linear \(\lambda\)-term and, equivalently, that every BCK-combinator, has a type. This result, for BCK-combinators, was first stated as Theorem 1 by \textit{R. K. Meyer} and the reviewer [Logique Anal., Nouv. Sér. 28, 33-40 (1985; Zbl 0574.03004)], but the proof, based on an induction on the ``level'' of a combinator, does not show that this level is defined for all BCK combinators. (The reviewer has since overcome this problem by a combinator based method.) The present paper translates the combinators into linear \(\lambda\)-terms, for which the induction becomes simply one on length.