# 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.