User talk:Blashyrkh/Between IJ and SK

Can we get the program? --Yayimhere2(school) (talk) 09:14, 24 January 2026 (UTC)

Sure, give me a couple of hours to sort some things out. The program is written in C, it reads BLC expression for X combinator candidate from stdin, then enumerates all expressions consisting of I, J and X, and beta-reduces them until K expression is obtained. BLC enumerator is written in python. --Blashyrkh (talk) 09:30, 24 January 2026 (UTC)

Done (the link is in the article text). To build:

cmake -D CMAKE_BUILD_TYPE=Release .
cmake --build .

I run it this way:

./enum-lambdas.py | grep CNL | cut -f1 -d' ' | ./between-IJ-and-SK | nl

Does John Tromp know the answer?

Funny thing is I'm sure Mr. Tromp knows the answer, he just thinks 'Ha, let the kids play a little longer' --Blashyrkh (talk) 20:24, 24 January 2026 (UTC)

Solution for X x = x (K x) x

The expression X T I, if I'm correct, gives this:

X T I
T (K T) T I
T (K T) I
I (K T)
K T

Which has already been solved in the table (#18).

Good point! Let's look at the whole picture:

  X = λ x . x (K x) x

  λ x y . J(J(JII))I(XTI)xy =
= λ x y . J(JT)I(XTI)xy =
= λ x y . JTI(JTx(XTI))y =
= λ x y . TI(Ty(JTx(XTI))) =
= λ x y . JTx(XTI)yI =
= λ x y . Tx(Ty(XTI))I =
= λ x y . (XTIy)xI =
= λ x y . (T(KT)TIy)xI =
= λ x y . (T(KT)Iy)xI =
= λ x y . (I(KT)y)xI =
= λ x y . (KTy)xI =
= λ x y . TxI =
= λ x y . Ix =
= λ x y . x =
= K
q.e.d.

I also have a question, how much is allowed in a combinator? Because if it can just be any lambda expression, then what to make of \x. x (ω K), or even Y K? –PkmnQ (talk) 01:59, 26 January 2026 (UTC)

Looks like you're right. Y K is Unlambda v combinator: it destroys its argument and returns itself. Black hole. Raw uncontrollable cancellability. We can pass it on, but sooner or later we apply it to some argument and get v again. There's no way to get K. So, we have to state this:

There are somethings between IJ and SK.

There are systems of combinators other than IJ (several ones, maybe infinitely many ones) that are non-complete and include IJ system as a subset. An example of such system is a system produced by IJ(YK) basis. It contains all non-cancellative combinators, but also YK itself and combinators that applies some of its arguments to YK. Another example is IJ(λ x . x (ω K)): the system contains (besides all non-cancellative combinators) only combinators none of which has normal form.

Do you agree with the statement? Is it okay if I put it to Talk:Combinatory logic where the question was initially asked? --Blashyrkh (talk) 06:26, 26 January 2026 (UTC)