What is the shortest function of lambda calculus that generates all functions of lambda calculus?

Solution 1:

I believe this is related to finding a single axiom base for intuitionistic propositional calculus. There is a web page by Ted Ulrich on the subject, which discusses many such axioms. However, trying to find the shortest single axiom corresponds to trying to find a combinator with the shortest type (as opposed to your goal finding a combinator with the shortest λ-calculus expression).

Edit: You can take those single axioms and ask Djinn (a Haskell theorem prover) to find functions with corresponding types. For example, taking one of the first axioms in Ted Ulrich's web page, you can ask Djinn:

Djinn> ? x :: ((p -> q) -> r) -> (s -> ((q -> (r ->  t)) -> (q -> t)))

and it answers

x :: ((p -> q) -> r) -> s -> (q -> r -> t) -> q -> t
x a _ b c = b c (a (\ _ -> c))

So expression λazbc.bc(a(λy.c)) has the given type, and it is a candidate for a single combinator you're looking for.

(It is not obvious how to express S and K from such a combinator, but it can be recovered from the proof that forumlas (p→(q→r))→((p→q)→(p→r)) and p→(q→p) can be derived from the single axiom.)

This way, you could generate many possible combinators and see how long they are. Most likely you won't find the shortest one, but you might find some that are shorter than the ones you described. If you do, let us know!

Solution 2:

I like $W = \lambda x.x K S K$ since it makes $K = W W W$ and $S = W (W W)$, although it is longer than either $U$ or $V$.