Skip to main content
1 of 3
John Tromp
  • 1.7k
  • 9
  • 15

Do Combinatory Logic bases need a function of 3 variables?

All the known bases of Combinatory Logic, such as {S,K}, or {K,W,B,C} have one or more combinators using 3 variables:

S = λxλyλz. x z(y z)
B = λxλyλz. x  (y z)
C = λxλyλz. x   z y

This begs the question whether we can make a basis with functions of only 2 variables. Surely if such a thing were possible, it would be a most interesting result and it would be well-known. But as far as I can tell, no such thing is known. Thus it seems nobody believes such a thing to be possible.

But has this been proven anywhere?

How do we know that {K,W,2,O,T,D} is not a basis, where

K = λxλy. x
W = λxλy. x y y
2 = λfλx. f(f x)
O = λxλy, y(x y)
T = λxλy. y x
D = λx. x x

?

John Tromp
  • 1.7k
  • 9
  • 15