Logic

Yeah and make sure to check out their patreon if you want to incentivize and support people living alternative lifestyles and creating things with love like this:

https://www.patreon.com/100

The webpage adds some unnecessary confusion by

1) using colored shapes instead of variable names.

2) (initially) presenting combinators as having 3 arguments, where they only need 1 or 2. So instead of the usual M x = x x, you see M x y z = x x y z.

One (improper) bird I find very interesting is the Starling's cousin S* x y z = x z (y (K z)), from which all other birds can be reconstructed.

(I think) this is a modern rendition of David Keenan's To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction [1], also linked in the OP. Perhaps you might appreciate the original better.

[1] https://dkeenan.com/Lambda/

Longer and more familiar tokens that don't all just look like piles of meaningless letters make it so a non-math person can follow it right up until they start taking about booleans. They totally lost me there. But I'm impressed that they explained it in a way that let me even get that far.

After that it starts not making sense without prior knowledge.

I vaguely remember something about there being no data other than functions, so I assume the values of true and false are represented by functions represented by birds?

What does a doubling one of the words have to do with an OR? I'm assuming that when you pass one of these birds to another bird, there's something special happening, and the mockingbird is no longer just repeating a value, and there's some kind of function composition happening?

Combinatory logic, underneath being lambda calculus.

For a simple explanation: think of `SKI` etc. as functions or transformations which do what is described, how they are described mathematically is discussed later. They act on all values, including each other. For this reason, they are called combinators, as combining them can give rise to any computation. Why that is is also discussed a bit later. Combinatoric application is left-associative, meaning that `SK` is equivalent to `S(K)` in more conventional mathematical notation.

For an easy example, think about the equivalence of the W-combinator and the expression SS(SK). If we apply some abstract values, say a, b, and c to these, we can make sure that the result is `a b b c`, keeping in mind that other combinators are a valid value for a combinator to take in:

    SS(SK) abc 
    → S a (SK a) bc 
    → a b (SK a b) c 
    → a b (K b (a b)) c 
    → a b (b) c = a b b c

Now if you want to read the definitions, you will need lambda calculus. It is basically an endless combination of two operations, one which is used to build and expression and one which is used to resolve it.

The most important is abstraction, which isn't explained in the post. You write a lambda (λ), the name of a bound variable (say, x), and then a full stop and the "body" of the abstraction. This can be thought of as a mathematical function definition, so that you can think of `f(x) = x` and `f := λx.x` as identical. Note, however, that the latter is anonymous and has to be assigned a name separately.

The second operation is application. This is left-associative, and we do not use parenthesis. `f x` is the same as `f(x)` in conventional notation. `(λx.x) y)` is then the application of `y` to `λx.x`. We replace the bound variable in the expression with the applied value: `(λx.x) y → y`.

We can create more complex multi-variable functions by nesting these:

    (λx.(λy.x)) 0 1 
    → (λy.0) 1 
    → 0 

The parentheses are redundant: `λx.λy.x`, and for notational sugar we contract the definition: `λxy.x`.

Armed with all of this, we can read the definitions of the "birds", or combinators:

    S := λxyz.x z (y z)
    K := λxyz.x z
    I := λx.x

Now it's possible to read the previously nonsensical notation in the article, both intuitively and by thinking open the relationships promised:

    W := SS(SK)
    → (λxyz.x z (y z)) S (SK)
    → λz.S z (SK z)
    → λz.(λxyz₂.x z₂ (y z₂)) z (SK z)
    → λzz₂.z z₂ (SK z z₂)
    → λzz₂.z z₂ ((λxyz₃.x z₃ (y z₃)) K z z₂)
    → λzz₂.z z₂ (K z₂ (z z₂)
    → λzz₂.z z₂ ((λxy.x) z₂ (z z₂))
    → λzz₂.z z₂ z₂

Now we can perform some tactical renaming (called α-conversion, we used this to avoid name collisions before):

    W := λxy.x y y

This is the official definition of the W-combinator and nearly the definition given to us, that being `W := λxyz.x y y z`. However, we can see that in application there is no difference:

    (λxy.x y y) a b c = (λxyz.x y y z) a b c
          → (a b b) c = a b b c
            → a b b c = a b b c

Hence, we consider these equivalent through something called η-reduction (`λx.E x = E` if `x` is not free in E). We can see, then, that each three of these systems can create any lambda expression, which are proven to be isomorphic to Turing machines. This is a powerful way to manipulate not only logic, but computation itself.

Not the best explanation, but I feel like introducing lambda calculus is necessary to truly intuitively understand how the operators manipulate each other.

The colored shapes are arbitrary symbols, variables like in algebra. They could be other combinators or anything in the system. Kx, for instance, always produces whatever x, a variable, happens to be when applied to something else. So KKI will produce K. KIS produces I.

So there is no one for one mapping. Any of those birds/combinators or some parenthesized expression of them can be put in place of the colored shapes.

Think of the "birds" (combinators) acting on a combined set of both the birds and the shapes. Don't forget that parenthesized blocks of birds and shapes are considered a single "letter" for manipulation. For an example of these in action, take this application to SS(SK), equivalent to W, with three inputs a, b, and c:

      -- reminder of the definitions
      Sxyz → xz(yz)
      Kxy  → x

      -- always expanding the leftmost combinator
      SS(SK)abc
    → Sa(SKa)bc
    → ab(SKab)c
    → ab(Kb(ab))c
    → abbc

The biggest leap to make is the first to the second line. S here is the x, a is the z, and (SK) is the y. Then with a little imagination you should be able to see that the expression morphed into xz(yz) with whatever wasn't touched, in this case bc, just kind of stuck on the end.

This also shows that the definition of the W-combinator given in the article

    Wxyz → xyyz

is a little overenthusiastic in having three arguments. The last one is actually never touched with the SK-definition!

    Wxy → xyy

would actually be enough, and it's the canonical definition for it when working with combinatory logic in a more serious context.

You don't need to distinguish KI (the kite) from KI (the kestrel followed by the idiot bird), because they evaluate to the same thing. Kite xy is y, and if you evaluate Kestrel Idiot xy, you get:

    KIxy -> Iy -> y

Similarly, because true is defined as K, and false as KI, if you evaluate Mxy where x and y are K or KI, and keep evaluating, you'll eventually end up with either K or KI, depending on whether (x or y) is true or false. I agree, though, that is confusing that the post didn't explain any of this; I assume it's not finished yet.