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