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)	Formula	K
1	000010	Xxy=y	JXI
2	0000110	Xxy=x	X
3	00000010	Xxyz=z	JIJIXI
4	000000110	Xxyz=y	JIIIX
5	0000000010	Xxyzw=w	J(JXIII)I
6	0000001110	Xxyz=x	J(JII)IX
7	0000011010	Xxy=yy	J(JXII)I
8	00000000110	Xxyzw=z	JXIII
9	00011000110	Xx=x(Kx)	JIJIXI
10	000000000010	Xxyzwv=v	J(JXIIII)I
11	000000001110	Xxyzw=y	JJII(JII)IX
12	000000011010	Xxyz=zz	J(JIJIXII)I
13	000001100010	Xxy=yI	J(JXII)I
14	000001110110	Xxy=xx	JIJIXI
15	000110000010	Xx=x(KI)	JIXJX
16	0000000000110	Xxyzwv=w	JXIIII
17	0000000011110	Xxyzw=x	J(J(JII))IXI
18	0000000110110	Xxyz=zy	J(J(JII))IX
19	0000000111010	Xxyz=yz	J(JXII)I
20	0000011000110	Xxy=y(Ky)	J(JXII)I
21	0000011100010	Xxy=xI	JIJIXI
22	0001100000110	Xx=xK	JIIIX
23	00000000000010	Xxyzwvu=u	J(JXIIIII)I
24	00000000001110	Xxyzwv=z	J(JXIIIII)I
25	00000000011010	Xxyzw=ww	J(J(JXIII)II)I
26	00000001100010	Xxyz=zI	J(JIJIXII)I
27	00000001101110	Xxyz=zx	J(JIJIXII)I
28	00000001110110	Xxyz=yy	J(JXIII)I
29	00000001111010	Xxyz=xz	JIJIXI
30	00000101101010	Xxy=yyy	J(JXII)I
31	00000110000010	Xxy=y(KI)	JXIJI
32	00000110001110	Xxy=y(Kx)	JXIJI
33	00000110011010	Xxy=y(yy)	J(JXII)I
34	00000111000110	Xxy=x(Ky)	JIIIX
35	00011000000010	Xx=x(K(KI))	JIJXXI
36	00011000001110	Xx=x(K(Kx))	J(JIXIX)I
37	000000000000110	Xxyzwvu=v	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)