Is there a proof of (non)existence of a proper universal combinator?

420 Views Asked by At

It is a well-known fact that all combinators can be derived from the two fundamental combinators K and S. It seems only natural to also ask whether there is a single universal combinator, but I can’t find much information on the topic. The only examples of universal combinators I can find are improper ones that refer to other combinators in its definition, such as Chris Barker’s U combinator. I also found a discussion about the same question, but no definitive answers are offered there.

Is there a proof of (non)existence of a proper universal combinator, one that can be defined purely in terms of its own variables?

1

There are 1 best solutions below

1
On BEST ANSWER

You are looking for Craig's theorem, which states that that there is no single proper combinator that is a basis for combinatory logic.

(Craig's theorem is not any more general than that.)

One reference is A new proof for Craig's theorem by Patrick Bellot. I have not been able to find the entire paper online, only the abstract; if I find a better reference I will add it here.

(Unfortunately, it seems there is a much better-known Craig's theorem in mathematical logic which is completely unrelated. I have written to Bellot for details.)

Addendum 2016-03-09: The Bellot proof is only one page long, and is now available from JSTOR for free online viewing. The citation given by Bellot is:

H.B. Curry and R. Feys (with two sections by W. Craig), Combinatory Logic, Vol 1, North-Holland, Amsterdam, 1958.

but he says that this proof “was shown to be incomplete by André Chauvin”.