The Y Combinator (no, not that one) – A Crash Course on Lambda Calculus

Thanks for letting me discover the work of that man. Its approach to learning about something by actually doing it really shines in the video you linked.

If anyone hasn't seen this I highly recommend it, if not just because Weirich was a great guy and was very entertaining. RIP.

Thanks for this. I just learned a lot!

Great video, I was hoping it would be linked here. Jim's is not only an informative talk but an inspirational ability to teach.

There are only two bits of syntax for lambda calculus: 'application', written "a b", and 'abstraction', which I'll write as "\a. b" (since "\" is easier to type than lambda). The words "abstraction" and "function" are pretty-much interchangable, although we might use "abstraction" to specifically refer to a "new" function definition, like this:

    \x. x

As opposed to a "calculated" function, like the result of an application:

    a b

Regarding precedence, application is "left-associative", meaning that

    a b c

is the same as

    (a b) c

Abstractions 'capture' everything after the ".", so

    \a. b c \d. \e. f

is the same as

    \a. (b c \d. (\e. f))

You need to use parentheses to go the other way, eg.

    a (b c)
    (\x. x) y

In the case of the Y combinator, there is only one "f" variable but it gets used twice. There are two "x" variables, one per abstraction, although those abstractions just-so-happen to look the same. In other words, we could replace one of the "x" abstractions with "\y. f (y y)" (known as an "alpha conversion") but we can't rename one of the "f"s without renaming all three occurences.

Regarding your last point, the only semantic values in lambda calculus are functions, so "t" can't be anything else. However, we just saw that there are two syntactic forms which "t" can take. If "t" is an abstraction, we can simplify our expression immediately via the beta-reduction rule ('applying t to s').

If "t" is an application, like "t1 t2", then we can try simplifying that to get either an abstraction (which we can apply to "s") or another application, which we can try simplifying, and so on.

It's possible (due to the Halting Problem) that we keep getting applications no matter how much we try to simplify, in which case we've hit an infinite loop while trying to calculate "t", and hence we can never reach the point where we can apply it to "s".

Since SICP and Lambda papers I have a fascination for the relationship with discrete math, computing devices and their topology. This doesn't help.

Also, and a big also, the Y-combinator exists in (untyped) lambda calculus---e.g. all you need is abstraction and application.

This came as a shock to Church when he invented it as he wanted to use LC as a language for mathematical logic and fixed point combinators spell out doom for logical purposes. He thus invented the simply typed lambda calculus to banish such constructions.

Still wishing more people read that book. It is not overrated.

I actually complained about this on twitter a while ago, and pg said he didn't believe me - recommending "y combinator lambda" as a search string. But more specific things like "y combinator golang" require you to block HN and a few other sites to get meaningful results.

Hey. You're completely missing it. The Y combinator shows that full general computation, including recursion and iteration, derives automatically and inevitably from just basic rewrite rules. Obviously it is too raw to be used directly. But if you design/implement any system with rewrite rules, you have provided indefinite power for recursions, and you have opened the Pandora box of undecidable-termination. This means that decidable computation can only occur without rewriting, which is incredibly restricted.

Food for thought.

It has some minor uses, but not a whole lot. If, for example, you wanted to do recursion with an anonymous function, you could use the Y combinator (well, more likely the Z combinator which is a variant of the Y combinator that works with strict evaluation). However, it'd probably just be easier (and clearer!) to give the function a name and do it that way.

However, as someone pointed out, the Y combinator's utility is not as an actual tool for programmers but as a tool for mathematicians working in computational mathematics. Alonzo Church solved the Entscheidungsproblem using a primitive variant of the Y combinator called the omega combinator. The Y combinator itself was invented by Haskell Curry (his name is familiar for a reason) in order to demonstrate what is commonly called Curry's paradox.

Well, in 1936 Church invented the LC in order to serve as a foundational logic for mathematics. This was around the time that Hilbert's Program was attempting to totally mechanize reasoning through rich logical languages and Church wanted to use LC to define the notion of "efficiently computable" which was part of Hilbert's specification.

The Y-combinator was discovered originally as a flaw in the LC. It meant that you couldn't use LC as a logical language because you could form infinite loops which are not just not efficiently computable (in a sense, har har) but also correspond to vacuous logical statements like "If A proves A then A is true" which, in the context of rules like reflexivity "If A then A" (provable in LC as λ x . x) is logical nonsense.

To be more clear, here's the Y combinator

    λ f . (λ x . f (x x)) (λ x . f (x x))

and here's the Y-combinator applied to `id = λ x . x`

    (λ x . (x x)) (λ x . (x x))

which reduces into itself—a dead loop and a logical inconsistency (named "omega" as the end of LC!)

Anyway, Church worked for the next 4 years to invent the Simply Typed Lambda Calculus which imposes a Russell-like typing discipline on the LC in order to outlaw the Y-combinator. This made LC more useful for logic (and indeed STLC models Gentzen's Natural Deduction logical system) but it threw away its ability to compute any "recursively enumerable" function. That latter thing was what eventually came to be the definition of "efficiently computable" (after corroboration between Church's LC, Turing's Turing Machines invented the next year).

And now we happen to care about writing programs which, in general, may be r.e. and so we use either untyped LC or typed LC which has logically unsound recursion principles.

Yes, it is useful. For example, if you want to bootstrap a language implementation from the smallest possible subset, with a very trivial interpreter, then using Y-combinator as a way to implement recursion is reasonable (after all, performance does not matter for the bootstrap phase). See an example of such a use in https://github.com/combinatorylogic/mbase/blob/master/src/l/...

Named recursion requires a notion of time, which is clear from your distinction between "permanent" and "temporary" names. This can add unnecessary complexity.

Let's use an analogy: is it ever useful to call a function with another function's return value?

    p = \q. f (g q)

We can implement the same thing using named arguments with permanent or temporary names, for example:

    p = \q. let g_of_q = g q
             in f g_of_q

That forces us to write the same boilerplate every time. We can do better by encapsulating it in a function (DRY):

    compose = \a. \b. \c. let b_of_c = b c
                           in a b_of_c
    p = compose f g

The Y/Z combinators do exactly the same job as compose, except for self-application rather than chained application. They let us write down what we mean, directly, without having to break it up into artificial chunks and chain them back together. Notice that the final definition of "p" doesn't even need a lambda abstraction, since the function is being calculated automatically rather than defined manually.

For example, I've used the Z combinator when defining arrays of functions in PHP. Without it, I'd have to define the functions separately, using brand-new function abstractions to inherit the self-reference (which is horribly verbose in PHP), then combine them into an array; or I'd have to define them separately, using brand-new function abstractions to inherit the array, then combine them into the array. Either way, it would add a bunch of complexity and boilerplate.

Nice catch, thank you. I've fixed it now. :)