What the fuck is lambda calculus?

Draft::What the fuck is lambda calculus?

$$ \lambda f.(\lambda x.f(x x))(\lambda x.f(x x)) $$

Fuck

Lambda calculus.

It's a concept we've all heard about. The more brave among us might have even read the Wikipedia article. Inevitably we close the page and retreat back to the warmth of our Vim buffers. The if err != nil scattered around our Go code remind us that everything will be okay. "It doesn't matter" you announce to no one in particular, although you were kinda hoping that barista heard anyway.

Well, you're not wrong. I guess it doesn't really matter. We're fully capable of writing and reasoning about complex computer programs without understanding lambda calculus.

If you're curious, I encourage you to continue. Many of these concepts bend the mind and might make you appreciate computing and math from a newfound perspective. You might even finally be able to hang with the cool kids over at HackerNews.

Before We Embark

I'm going to present math and programming examples exploring the fundamentals of lambda calculus. The goal is to consider computing in its sexy abstract sense. On the journey, we will derive and explore concepts in this domain - trying to arrive at each result naturally.

Don't worry about speed or efficiency. Time is a meaningless construct anyway.

Don't worry about readability. This will be the least readable code you've ever seen.

This is a thought exercise. When all is said and done, what do computers and programming languages really need?

This article will be dense at times. Don't be afraid to re-read certain sections or come back another day if a particular concept isn't clicking.

Some History

Lambda calculus was first explored by a smart fellow named Alonzo Church in a series of papers published in the 1930s. Although his initial findings were proven to be logically inconsistent, he stripped out everything unrelated to computation and gave us untyped lambda calculus in 1936.

Also in 1936, Alan Turing independently (yea right, he totally googled that shit) created a theoretical model for machines that could carry out computations by manipulating symbols on a single dimensional tape.

A function is said to be $\lambda$-computable if a function on Church numerals (just think of these as the number system of lambda calculus) can be represented via lambda calculus.
A function is said to be Turing computable if some Turing machine computes the same function on its own encoded numbers (why aren't these called Turing numerals?).

_{"I'm smarter than all of you" - Alonzo Church, probably}

Long story short, they joined forces and proved that a function is $\lambda$-computable if and only if it is Turing computable. They took it one step further and suggested that anything that is effectively calculable, that is to say 'can be calculated', can also be calculated using lambda calculus.

Doesn't that sound kind of familiar? Oh yea - Turing completeness is an attribute of a model of computation (read: programming language) if said model can successfully simulate a Turing machine which in turn can simulate anything effectively calculable.

This has pretty amazing consequences. For example, since untyped lambda calculus uses only anonymous functions (more on this later) you should be able to express any sort of computation you want using only this. You'll soon see why that matters.

These concepts in turn influenced many aspects of computer programming - namely the design of the early (and even modern) programming languages. Many programming languages' computational models can be understood in terms of lambda calculus.

Some 'Math'

Lambda calculus isn't really math in the same sense that classical calculus is. In fact it's more akin to computing and logical formalism. If you're as bad at math as most software engineers, you'll find that heartening to hear.

Let's derive the set of all lambda terms, $\Lambda$, recursively:

Any variable $x \in \Lambda$
If $M \in \Lambda$ and $x$ is a variable, $(\lambda x.M) \in \Lambda$
If $M, N \in \Lambda$ then $M N \in \Lambda$

Okay that probably doesn't help. Let's list some examples instead:

$x, y$ are valid $\lambda$-terms
Since $y$ is a valid $\lambda$-term, $\lambda x.y$ is a valid $\lambda$-term
Since $\lambda x.y$ is a valid $\lambda$-term, $(\lambda x.y)(\lambda x.x)$ is a valid $\lambda$-term

Okay... that still doesn't help a lot. Let's examine some specific cases:

$\lambda x.x$ is the identity function since it maps $x$ -> $x$
$\lambda x.y$ is a constant function since it maps $x$ -> $y$ no matter what $x$ is

Hold up - when did functions enter the picture? The term function here is loosely defined. In fact, in the earlier descriptions of lambda calculus, the $\lambda$ symbol is simply treated as an abstraction operator that binds variables into the body of the abstraction. The distinction between bound and free variables will become important shortly.

Thus you can think of chained $\lambda$-expressions as a series of partial/curryed functors that simply substitute/apply their bound variable forward in the chain.

Cool - we have functions. Notice they're all anonymous, i.e. $\lambda$-terms are just arbitrarily long chains of these simple building block expressions. Remember the Church-Turing Thesis on $\lambda$-calculus being able to calculate anything effectively computable? Now that you see how simple this formalism is, the abstract beauty of this whole topic becomes apparent.

What about all that nonsense with free and bound variables? Well, that's how you actually apply functions to values. You do want to be able to do that, don't you?

Some Code

Guess what! The code portion is in Clojure, if only to confuse you more. In reality I chose Clojure for a few reasons:

Compact lambda syntax (R/Python are too verbose which actually make it more complicated to follow along)
Using something LISPy (not functional, I hate that term) might help you appreciate these examples even more
I want as few people to understand this post as possible
I want to be as impractical as possible.
- _{Before the Church of Clojure nails me to a cross, I should say that I am joking}

In retrospect, using a LISP both overstates and understates the elegance of the following results. The code looks more intuitive and rational in Clojure compared to, say, Python and thus may not blow your mind as much. However that's probably a good thing for really understanding this concept.

Feel free to rewrite these in any language that supports higher order functionals which is, shockingly, every modern language.

_{"A function has no name" - Jaqen H'ghar}