Live data from Hacker News

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

medium.com

41–50 of 51 posts

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

#41
post #23

Earlier quoted context omitted.

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 y…

Can you recommend me to any further reading regarding this or good literature? I've always meant to keep up with that, but aside from source papers is there a good overview of essentially what you're explaining? ie Further reading about Hilbert's Program.

The Stanford Emcyclopedia of Philsophy is usually a good source. If you're in Boston I'm going to be giving a Papers We Love talk on this stuff next week.

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

#42
Nice article, definitely piqued my interest in the lambda calculus, but there were a few points that were confusing for me as my first glimpse at the lambda calculus.

The first confusing point was the lack of definition of the order of operations. I first stumbled at the line (λy.(λx. x) y) a b . Is this supposed to be (λy.(λx. x) y) (a b) or ((λy.(λx. x) y) a) b . In this case both give the same answer, but it's not obvious that associativity holds in general.

It gets worse with the Y combinator: λf. (λx. f (x x))(λx. f (x x)) . Is this (λf. (λx. f (x x)))(λx. f (x x)) or λf. ((λx. f (x x))(λx. f (x x))) . Peeking ahead, it seems to be the latter, which makes more sense (otherwise the letter f would be pressed into service in two different contexts), but it's totally ambiguous from the rules that have been presented in the article.

The other point of confusion was regarding rule #3 (If t and s are both valid λ-terms, then t s is a valid λ-term.) The article tells is a certain manipulation we can do if t is a "function" (i.e. something that begins with a λ, I don't know the technical name for this), but doesn't say what to do if t is not a "function". As far as I can tell the answer is: do nothing, there is no simplification in this case. It would be nice if this was said explicitly.

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

#43
post #30
post #14

Earlier quoted context omitted.

I do use it directly. For example in Fexl I define the append function for lists as: \append=(@\append\x\y x y \h\t [h; append t y]) Where '@' is the Y-combinator. Note that there's no direct self-reference with the symbol "append" there. I could define it equivalently as: \append=(@\loop\x\y x y \h\t [h; loop t y])

Why? Is it unreasonably difficult for you to implement recursion via direct self-reference in your language? Or do you just not want to because the Y combinator is there and it's cool?

True, I could implement it in terms of direct self-reference. At one point I used the "==" syntax for just that purpose:

    \append==(\x\y x y \h\t [h; append t y])
Maybe I should resurrect that syntax option. :)

It was trivial to implement. When the parser sees the "==", it just automatically abstracts the symbol "append" from the definition and applies the fixpoint operator (Y combinator).

The only reason I eliminated "==" in the first place was that I was in the throes of using different syntaxes for lazy, eager, and self-referencing definitions. Now I've settled in on "=" always meaning eager evaluation, without exception. Then I got hyper-minimalist and said that's it, there's only one syntax for definitions, and it's "=", and if you want self-reference, use "@".

However, the decision to settle in on eager evaluation now frees up "==" once again as an option for self-reference. So I may bring that back.

Thanks for the food for thought.

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

#44
post #43
post #30

Earlier quoted context omitted.

Why? Is it unreasonably difficult for you to implement recursion via direct self-reference in your language? Or do you just not want to because the Y combinator is there and it's cool?

True, I could implement it in terms of direct self-reference. At one point I used the "==" syntax for just that purpose: \append==(\x\y x y \h\t [h; append t y]) Maybe I should resurrect that syntax option. :) It was trivial to implement. When the parser sees the "==", it just automatically abstracts the symbol "append" from the definition and applies the fixpoint operator (Y combinator). The only reason I eliminated…

Postscript: You might well ask why not just use "=" only, and assume that all definitions are potentially self-referencing?

That's a non-starter because I find that redefinition is the more common intent:

    \x=4
    \x=(* x 5)
    \x=(+ y x)
In those cases I don't want x defined in terms of itself, but rather in terms of the previous definition of x.

That is why I would insist on a special token such as "==" to express the intention of self-reference.

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

#45
post #42

Nice article, definitely piqued my interest in the lambda calculus, but there were a few points that were confusing for me as my first glimpse at the lambda calculus. The first confusing point was the lack of definition of the order of operations. I first stumbled at the line (λy.(λx. x) y) a b . Is this supposed to be (λy.(λx. x) y) (a b) or ((λy.(λx. x) y) a) b . In this case both give the same answer, but it's not…

[deleted]

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

#47
post #42

Nice article, definitely piqued my interest in the lambda calculus, but there were a few points that were confusing for me as my first glimpse at the lambda calculus. The first confusing point was the lack of definition of the order of operations. I first stumbled at the line (λy.(λx. x) y) a b . Is this supposed to be (λy.(λx. x) y) (a b) or ((λy.(λx. x) y) a) b . In this case both give the same answer, but it's not…

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".

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

#48
post #37

Earlier quoted context omitted.

">derives automatically and inevitably from just basic rewrite rules." I said "full general computation, including recursion and iteration, derives automatically and inevitably from just basic rewrite rules". You can't cut a sentence wherever you want and still think you're responding to the original thought. There is an imprecision in my original comment, but it's not there. If you can stop nitpicking long enough, y…

Thanks for the assertion that everybody can understand you when you use terms without defining them. Not everybody here is so lucky as to have the same educational background as you. What is a rewrite rule? To me, it's something you put in a web server configuration.

My apologies, I was only responding to the previous comment, forgot momentarily about others, sorry about that. Let me try to fix this.

A computation engine based on rewrite rules, in general, performs computations by replacing instances of certain patterns by some other patterns. Patterns can be literal or generic. The rules according to which these rewrites are done are "code" of the computation, they determine what computation the system performs. Different rules can result in a system that may do one of: computing prime numbers, computing digits of pi, factoring large number in prime divisors, finding the shortest path visiting all cities exactly once in a given map, rendering a 3D scene from a list of objects and coordinates, finding the best potential dating matches for a given user out of list containing many other users, or outputting a Schonberg-style tonal composition in waveform with synthetic piano-like sound.

The lambda calculus is one such type of computation system. The core element is a lambda expression of the form (\x.y), where "\" is just ASCII for the greek lambda letter which is hard to type for me now. The core thing a lambda-calculus system does is it takes lambda expressions and it applies a simple rewrite rule: where there is a sequence of the form (\x.y)z, where x,y,z can be anything, it will substitute the whole thing by "y", but wherever "x" appears inside "y", it will write "z". For example:

  (\x.xx)A
Will be rewritten to:

  AA
Given an initial string, the engine that computes the lambda expression will apply this rewrite rule repeatedly until no more rewrites can be done. This may or may not reach an end (this is the halting problem - in a general case, it is impossible to know whether the computation will reach an ending point or not).

The rewrite rule is called "beta reduction", by the way, but try to remember the concept, not the name, which is arbitrary and unimportant.

Using lambda notation you can craft code that will do any of the things above. The code will look like a long lambda expression, which the lambda-calculus engine can work on following the standard rules to end up producing the end result.

The Y combinator is a specific (\x.y) lambda expression that, once applied to some value by the rewriting system, it results in a computation being done on that value, plus an extra copy of the Y combinator, thus allowing a new iteration of the same computation. Thus resulting in being able to keep on computing - thus being able to compute anything requiring arbitrary recursion, such as the factorial of a number, the Ackerman function, the shortest path in an arbitrary graph, or whatever.

Although I've never seen Paul Graham explain it, my take is that the accelerator is called Y Combinator because they put some money in, this allows the startups to get to profitability, they get their money back, and they can use it again to fund new startups, thus achieving infinite effective resources from finite initial resources.

PS: the author of the original comment was handwaving and nitpicking since he didn't like being in the point of having missed something (which we all do quite often, incidentally, including myself in the previous comment). I don't like that behavior and I don't like the time and energy waste it results in, thus my dismissive response, apologies everyone for not responding constructively.

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

#49
post #2

One of my favorite programming videos: Jim Weirich on the Y Combinator https://www.youtube.com/watch?v=FITJMJjASUs

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

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

#50
post #42

Nice article, definitely piqued my interest in the lambda calculus, but there were a few points that were confusing for me as my first glimpse at the lambda calculus. The first confusing point was the lack of definition of the order of operations. I first stumbled at the line (λy.(λx. x) y) a b . Is this supposed to be (λy.(λx. x) y) (a b) or ((λy.(λx. x) y) a) b . In this case both give the same answer, but it's not…

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 applic…

>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".

But note that the _order_ of the reductions doesn't matter, as long as they're valid reductions. We always get the same result or it never halts like you said.

https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem

The Church-Rosser theorem probably deserves its own blog post.

Post reply on HN