In computer science, we know a function has an arity. And we noticed the similarity between function and a term in combinatory logic, so could we define the arity of a term in combinatory logic? And also could we consider some inference rules?
By definition, we have:
$Ix \rightarrow x$
$Kxy \rightarrow x$
$Sxyz \rightarrow xz(yz)$
These definitions may lead us to think:
- arity of I is unary
- arity of K is binary
- arity of S is ternary
If these are held, we may say $\iota$ is an unary term where
$ \iota x \rightarrow xSK$
But it cannot easily judge that
- $\iota \iota \rightarrow I$, and then it is unary
- $\iota (\iota (\iota \iota)) \rightarrow K$, and then it is binary
- $\iota (\iota (\iota (\iota \iota))) \rightarrow S$, and then it is ternary