BCK-combinators and linear -terms have types
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.
- Phase semantics and Petri net interpretation for resource-sensitive strong negation
- Filter models with polymorphic types
- Principal types of BCK-lambda-terms
- Perpetual reductions in -calculus
- On principal types of combinators
- A type-assignment of linear erasure and duplication
- Weak linearization of the lambda calculus
- The number of proofs for a BCK-formula
- scientific article; zbMATH DE number 3916223 (Why is no real title available?)
- The Relevance Graph of a BCK-Formula
- Compact bracket abstraction in combinatory logic
- scientific article; zbMATH DE number 1497851 (Why is no real title available?)
- scientific article; zbMATH DE number 7029315 (Why is no real title available?)
- The proofs of α → α in P – W
- Abstract families of abstract categorial languages
- Strong typed Böhm theorem and functional completeness on the linear lambda calculus
- Principal type-schemes of BCI-lambda-terms
- On the reification of semantic linearity
- Linear additives
- Principal types as partial involutions
- Gödel's system T revisited
This page was built for publication: BCK-combinators and linear \(\lambda\)-terms have types
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1119620)
