10
$\begingroup$

I suspect there's a good chance the answer to this is unknown and hard (or at least extremely tedious), but I figured it would be worth asking.

It's well known that the functions $K:=\lambda x.\lambda y.x$ and $S:=\lambda x.\lambda y.\lambda z.xz(yz)$ together generate all functions of lambda calculus.

It's also possible to do it with just a single function, as mentioned here: If we define $U=\lambda x.xSK$, then we can obtain $K=U(U(UU))$, and $S=U(U(U(UU))$, and thus everything.

It's also possible to do this with $V:=\lambda x.xKS$, since $S=VVV$, and $K=V(VVVVV)$.

What I want to know is, picking a reasonable notion of "length", is there any way that is shorter than $U$ or $V$? Let's say for now that the length is the number of occurrences of a variable, including when they're introduced, so e.g., $K$ has a length of 3, $S$ has a length of 7, and $U$ and $V$ each have length 12. (Or is there a usual notion of "length" that's been studied?) Is it possible to do better than 12, and what's the shortest way?

What if we allow for more than one generator and total the lengths? Then the usual set $\{S,K\}$ does it with 10. (Should we add a penalty for using more than one? Well, I guess you could, but I'm not going to define it that way here. I mean, unless people have studied this problem and already doing it that way...). Can this variant be done in fewer than 10, and what's the shortest?

I don't expect there's any easy way to answer the "what's the shortest" question, but I'm hoping maybe that at least if there is a shorter way that someone will know it or find it.

2 Answers 2

6

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!

  • 1
    Are you sure there is a composition of this combinator that generates S or K? I tried running a systematic search but couldn't find one.2017-11-06
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$.