0

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
Mountain
  • 540
  • Your question is far from clear. What are you trying to achieve by classifying CL terms as unary, binary etc? What is $\iota$? Is it supposed to be (the translation into CL of) the $\lambda$-term $\lambda f.fSK$? – Rob Arthan Mar 14 '18 at 12:53
  • Hi, Rob, $\iota$ is a one-combinator basis of CL, and it is the $\lambda$-term $\lambda f . fSK$ – Mountain Mar 14 '18 at 13:07
  • 1
    Well, I think you've really answered your own question: it doesn't really make sense to assign rarities to CL terms: because (at least in untyped combinatory logic) you can apply any term to any other term. In typed combinatory logic, the types give a much stronger notion than arity that does make sense. – Rob Arthan Mar 14 '18 at 13:15
  • Thanks, I will check the related untyped and typed theories. – Mountain Mar 14 '18 at 13:54

0 Answers0