Combinatory abstraction using B, B′ and friends

AbstractIn this paper we characterise precisely the sets of terms whose abstractions can be defined using the following partial bases of combinators: {B, B′, I}, {B, B′, I, W}, {B, B′, I, K}, {B, T, I}, {B, T, I, W} and {B, T, I, I}. The reduction axioms for B′ and T are B′XYZY(XZ)TXYZYXZ. The first two B′-bases correspond via type-assignment to two interesting implicational logics. T has the re-ordering property of B′ but not its bracketing property, and turns out to be strictly stronger than B′ but strictly weaker than CI whose reduction axiom is CIXYYX