It is well known that the S and K combinators form a basis set for combinator calculus, in the sense that all other combinators can be expressed in terms of them. There is also Curry's B, C, K, W basis, which has the same property. There must be an infinite number of such bases, but I don't know of any others.
I am aware that there are a number of single-combinator bases, such as the Iota combinator and the various others constructed/reviewed by Fokker. However, these are "improper" combinators, meaning that they are expressed in terms of other combinators rather than pure abstractions.1 For the purposes of this question I'm interested only in basis sets composed of proper combinators.
Does there also exist a study of the other possible basis sets? Ideal would be something along the lines of Wolfram's study of various other models of computation, in which the various combinations are studied systematically. In particular, I'm interested in whether simple examples of the following things are known:
- A minimal basis set that includes the I combinator. (I'm using "minimal" to mean that if you remove any member it stops being a basis, so the SKI basis would not count.)
- A minimal basis set that includes the Y combinator, or the $\omega$ combinator (aka mockingbird)
Any other information about other possible bases for combinatory logic besides S, K and B, C, K, W would be really helpful.
As a broader point, I'm interested in the study of the combinatory calculus as a purely mechanical system, i.e. as a set of transformation rules on binary trees with labelled nodes, which need not be given any particular semantic interpretation. Any pointers towards resources that take this approach would be greatly appreciated. (To Mock a Mockingbird takes this approach but gives an incomplete presentation, whereas Barendregt's the Lambda Calculus is very much tied to semantics, making it hard for me to extract the purely mechanical aspects that I'm interested in.)
1To be precise: in lambda calculus a proper combinator is an expression of the form $(\lambda.x_1x_2\dots P(x_1,x_2,\dots))$, where $P(x_1,x_2,\dots)$ only has $x_1$, $x_2$ etc. as free variables, and does not contain any abstractions. So for example, $(\lambda x y z. x(z z))$ is a proper combinator, but $(\lambda x. x(\lambda y.y) )$ is not, because it contains $x$ applied to a lambda term.