User:Blashyrkh/Between IJ and SK

Is there a non-complete system of combinators that includes IJ system as a subset? Equivalent: is there a cancellative combinator X for which K combinator can't be expressed in IJX basis?

The opposite question: is it enough to add any cancellative combinator to IJ basis to make the basis complete? Or, equivalent: is it possible to express K combinator in IJX basis for any cancellative combinators X?

I have no proof yet. Not a tiniest idea what the proof might be.

I made a program (github) that searches for expression of K combinator in the given IJX basis, and I'm going to post the results here.

K in IJX basis

#	X (BLC syntax)	K
1	000010	JXI
2	0000110	X
3	00000010	JIJIXI
4	000000110	JIIIX
5	0000000010	J(JXIII)I
6	0000001110	J(JII)IX
7	0000011010	J(JXII)I
8	00000000110	JXIII
9	00011000110	JIJIXI
10	000000000010	J(JXIIII)I
11	000000001110	JJII(JII)IX
12	000000011010	J(JIJIXII)I
13	000001100010	J(JXII)I
14	000001110110	JIJIXI
15	000110000010	JIXJX
16	0000000000110	JXIIII
17	0000000011110	J(J(JII))IXI
18	0000000110110	J(J(JII))IX
19	0000000111010	J(JXII)I
20	0000011000110	J(JXII)I
21	0000011100010	JIJIXI
22	0001100000110	JIIIX
23	00000000000010	J(JXIIIII)I
24	00000000001110	J(JXIIIII)I
25	00000000011010	J(J(JXIII)II)I
26	00000001100010	J(JIJIXII)I
27	00000001101110	J(JIJIXII)I
28	00000001110110	J(JXIII)I
29	00000001111010	JIJIXI
30	00000101101010	J(JXII)I
31	00000110000010	JXIJI
32	00000110001110	JXIJI
33	00000110011010	J(JXII)I
34	00000111000110	JIIIX
35	00011000000010	JIJXXI
36	00011000001110	J(JIXIX)I
37	000000000000110	JXIIIII

I see no reason to post search results anymore, they prove nothing. But I'm not going to stop the program, let it run. Who knows, maybe it finds some X for which no IJX-expression beta-reduces to K, that would be interesting. Meanwhile I'm thinking about the proof.

---

Some ideas for the proof

The program has stuck at this:

X x = x(Kx)x (BLC: 000101100011010)

I have no idea how to squeeze K (or anything cancellative) from it. Maybe the program will find anything, but I doubt it.

---

Case 1. Consider a proper cancellative combinator:

X = λ x1x2...xn.<some application of xk1...xkj>, where k1...kj<n

X I(1) ... I(n-1) xn = I, so

X I(1) ... I(n-1) = λ xn . I = KI

K = J(KI)I = J(XI(1)I(2)..I(n-1))I

Case 2. Consider a proper cancellative combinator:

Y = λ x1x2...xn.<some application of x1...xi-1,xi+1...xn>

Let's introduce a combinator:

F(i,n) = λ f x1...xn . f x1...xi-1xnxi+1...xn-1xi

F^(i,n) effectively swaps i'th and n'th arguments of a given function. Such combinator is non-cancellative, so it can be expressed in IJ basis. E.g.:

F(1,2) = λ f x1 x2 . f x2 x1 = C = J(JII)(J(JII))(J(JII))
F(1,3) = λ f x1 x2 x3 . f x3 x2 x1 = F* = J(JII)(J(J(JII)))(J(JII))
F(2,3) = λ f x1 x2 x3 . f x1 x3 x2 = C* = J(J(JII))(J(JII))(JI(J(JII)))
... and so on ...

Then X = F(i,n) Y is a combinator that satisfies the case 1 above:

K = J(F(i,n) Y I(1)I(2)..I(n-1))I

Case 3. Consider a proper cancellative combinator:

 Z = λ x1x2...xn.<some application of xk1...xkj,xi+1...xn>, where k1,...kj<i

So, proper combinator Z destroys several input variables, and i is the highest index of variables destroyed by Z.

Then X = F(i,n) Z is a combinator that satisfies the case 1 above:

K = J(F(i,n) Z I(1)I(2)..I(n-1))I

Case 4. TODO: non-proper cancellative combinator like λx.xK

TODO: the idea is to give it not just I's but specially prepared F^(i,j)'s to extract internal cancellative combinators and cancelling (with their help) all the rest garbage. Still thinking...

TODO: we should be ready to such non-trivial cases like λxy.yS(xK) . So, passing I as y is not a good idea because it reveals S which in this position acts as a function and not as a parameter which can be ignored/swapped out. y should be F^(foo,bar) to pass execution to x.

TODO: maybe, inner expression of the lambda should be represented as a binary tree, and processed from left to right???

TODO: another (and even less trivial) case is λx.xS(xK) . Here we should choose x wisely because it must deal differently with S and with K (how is it called? multiprogramming? smth like this)