# A one-combinator base for Combinatory Logic

Let's find a combinator 𝜟 such that 𝜟 𝜟 = 𝐊 and 𝜟 𝐊 = 𝐒.
If such a combinator exists, it forms a base for the Combinatory Logic.

Let's assume 𝜟 has the form `𝐃 𝛼 𝛽` where 𝐃 is the constructor of pairs (i.e. 𝜟 has the form ⟨𝛼,𝛽⟩).

The 𝐃 combinator is defined as:

𝐃 𝑥 𝑦 𝑡 = 𝑡 𝑥 𝑦 

We want to have 𝜟 𝐊 = 𝐒, so it must be:

 𝜟 𝐊 = 𝐃 𝛼 𝛽 𝐊 = 𝐊 𝛼 𝛽 = 𝛼 = 𝐒

which means that 𝛼 = 𝐒.

We want to have 𝜟 𝜟 = 𝐊 but we have:

𝜟 𝜟 = 𝐃 𝛼 𝛽 (𝐃 𝛼 𝛽) 
    = 𝐃 𝐒 𝛽 (𝐃 𝐒 𝛽)
    = 𝐃 𝐒 𝛽 𝐒 𝛽
    = 𝐒 𝐒 𝛽 𝛽
    = 𝐒 𝛽 (𝛽 𝛽)

Since `𝐒 𝛽 (𝛽 𝛽)` is in normal form (it can't be reduced further) it can't be strictly equal to `𝐊`, however if we can find a combinator 𝛽 such that `𝐒 𝛽 (𝛽 𝛽)` *behaves* exactly as `𝐊`:

𝐒 𝛽 (𝛽 𝛽) 𝑥 𝑦 = 𝐊 𝑥 𝑦 = 𝑥

we can say that `𝜟 𝜟` is *extensionally equal* to `𝐊`.

A possible choice is `𝛽 = 𝐁 𝐊 𝐊 = 𝐊²` in fact:

𝜟 𝜟 𝑥 𝑦 = 𝐒 𝛽 (𝛽 𝛽) 𝑥 𝑦
        = 𝐒 𝛽 (𝛽 𝛽) 𝑥 𝑦
        = 𝛽 𝑥 (𝛽 𝛽 𝑥) 𝑦
        = 𝐁 𝐊 𝐊 𝑥 (𝐁 𝐊 𝐊 (𝐁 𝐊 𝐊) 𝑥) 𝑦
        = 𝐊 (𝐊 𝑥) (𝐁 𝐊 𝐊 (𝐁 𝐊 𝐊) 𝑥) 𝑦
        = 𝐊 𝑥 𝑦

We have so determined that `𝜟 = 𝐃 𝐒 (𝐁 𝐊 𝐊) = 𝐃 𝐒 𝐊²` and we have confirmed that exists a single-combinator base.

The original page in my old notebook: :smile: