BCK-combinators and linear \(\lambda\)-terms have types (Q1119620): Difference between revisions
From MaRDI portal
ReferenceBot (talk | contribs) Changed an Item |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0304-3975(89)90100-x / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1968532969 / rank | |||
Normal rank |
Latest revision as of 09:30, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | BCK-combinators and linear \(\lambda\)-terms have types |
scientific article |
Statements
BCK-combinators and linear \(\lambda\)-terms have types (English)
0 references
1989
0 references
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.
0 references
types
0 references
linear \(\lambda\)-term
0 references
BCK-combinator
0 references