Less Well-Known Cominatorially-complete Bases for Combinatory Logic

{S,N,C} Basis

I'm pretty sure that {S, N} is not a basis, less sure that {S, N, T} is not a basis. I could not get Prover9 to give me an expression acting as C, T or K.

rule: C 1 2 3 -> 1 3 2
rule: N 1 2 -> 2
rule: S 1 2 3 -> 1 3 (2 3)
abstraction: [_] *- -> C N 1
abstraction: [_] _ -> N N
abstraction: [_] *- _ -> 1
abstraction: [_] * * -> S ([_] 1) ([_] 2)
([a,b,c] a c b) first second third
([a,b,c] a (b c)) first second third
([a,b] a b b) first second

{S, N, C} basis code.

{B,W,C,N} Basis

Even though {S, N} probably isn't a basis, {B,W,C,N} does constitute a basis, since C N acts like K, even proceeding via head reduction. .

rule: B 1 2 3 -> 1 (2 3)
rule: W 1 2 -> 1 2 2
rule: C 1 2 3 -> 1 3 2
rule: N 1 2 -> 2
abstraction: [_] *- -> C N 1
abstraction: [_] _ -> N N
abstraction: [_] *- _ -> 1
abstraction: [_] *- *+ -> B 1 ([_]2)
abstraction: [_] *+ *- -> C ([_]1) 2
abstraction: [_] * * -> W (B (C ([_]1)) ([_]2))

{B, W, C, N} basis code.

{B, C, I, F} Basis

Would {S, F, I} work as a basis?

rule: B 1 2 3 -> 1 (2 3)
rule: C 1 2 3 -> 1 3 2
rule: I 1 -> 1
rule: F 1 2 -> 1 1
abstraction: [_] _ -> I
abstraction: [_] *- -> C (F I) 1
abstraction: [_] *- *+ -> B 1 ([_]2)
abstraction: [_] *+ *- -> C ([_]1) 2
abstraction: [_] * * ->  C (B (C F (C F)) (C C)) (B (C ([_]1)) ([_]2))

F makes up half an Ogre (or Egotistical Bird): F F a b c ... x y z ->* F F This F is not Barry Jay's factorization F.

{B, C, I, F} basis code.

{B',W,K} Basis

From "Combinatory Logic", vol 1, Sec 5S2, page 185 in the copy I used. Curry & Feys did not give an abstraction algorithm, just defined I, B, C, S in terms of B', W, K to prove combinatory completeness.

rule: B' 1 2 3 -> 2 (1 3)
rule: W 1 2 -> 1 2 2
rule: K 1 2 -> 1
abstraction: [_] *- -> K 1
abstraction: [_] _ -> W K
abstraction: [_] *- _ -> 1
abstraction: [_] *- *+ -> B' ([_]2) 1
abstraction: [_] *+ *- -> B' ([_] 1) (W (B' (K 2))) 
abstraction: [_] * * -> W (B' ([_]1) (B' ([_]2)))

{B', W, K} basis code.