Example of append function reduced as combinators

Here's the definition of append using lambda variables:

\append == (\x\y x y \h\t item h; append t y)

Here's the definition without lambdas, using combinators:

\append = (Y ((R (L S)) ((R (R (L ((R R) item)))) L)))

We can view that combinatorial definition in two parts, like this:

\F = ((R (L S)) ((R (R (L ((R R) item)))) L))
\append = (Y F)

Now let's test the definition to see how it behaves.

: append x y
= Y F x y
= F (Y F) x y
= F append x y
= R (L S) ((R (R (L ((R R) item)))) L) append x y
= L S ((R (R (L ((R R) item)))) L append) x y
= S x ((R (R (L ((R R) item)))) L append) y
= x y ((R (R (L ((R R) item)))) L append y)

# At this point there are two cases:
# if x is end, then value is y and we're done.
# if x is (item h t), then we proceed with:

= item h t y ((R (R (L ((R R) item)))) L append y)
= R (R (L ((R R) item))) L append y h t
= item h (L append y t)
= item h (append t y)

That is indeed the correct value of (append x y), when x equals (item h t).