BCK-combinators and linear \(\lambda\)-terms have types
type: Item
instance of: scholarly article
title: BCK-combinators and linear \(\lambda\)-terms have types
zbMATH Open document ID: 0671.03010
DOI: 10.1016/0304-3975(89)90100-X
author: J. Roger Hindley
published in: Theoretical Computer Science
publication date: 1989-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 4097341
zbMATH Keywords: types
zbMATH Keywords: linear \(\lambda\)-term
zbMATH Keywords: BCK-combinator
reviewed by: Martin W. Bunder
MaRDI profile type: Publication
cites work: Q3691634
cites work: Q5565113
cites work: Linear logic
cites work: Combinatory Reductions and Lambda Reductions Compared
cites work: Q4722037
full work available at URL: 0304-3975(89)90100-x
OpenAlex ID: W1968532969
description: scientific article; zbMATH DE number 4097341