Live data from Hacker News

λ Calculus (2013) [pdf]

cs.rpi.edu

11–20 of 73 posts

Re: λ Calculus (2013) [pdf]

#11
post #10

Earlier quoted context omitted.

The Y combinator is not the same as λ calculus. The Y combinator is an expression in λ calculus.

The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.

> heart of the λ calculus

The Y combinator is a specific fixed-point combinator in lambda calculus. It is used to express recursion in lambda calculus where direct recursion is not initially available due to the lack of named functions. The Y combinator demonstrates the power of lambda calculus.

Re: λ Calculus (2013) [pdf]

#12
This PDF is an exerpt from the book Programming Distributed Computing Systems: A Foundational Approach by Professor Carlos Varela. He was my advisor at RPI, and one of the most pleasant professors I had the pleasure of interacting with during my time there. His classes were notoriously hard, but I enjoyed them very much. The full book includes very concise walk thoughs of various other less well known calculi and theoretical distributed programming models (in particular, the AMST lambda calculus actor model). If you like language or concurrency theory I highly recommend picking up a copy.

Re: λ Calculus (2013) [pdf]

#13
post #4
post #3

any idea what book this chapter is from?

Programming Distributed Computing Systems A Foundational Approach Carlos A. Varela 2013 https://mitpress.mit.edu/9780262018982/programming-distribut...

I had one of his classes. He really knows his stuff. Spoke fast, no filler, and had an answer prepared for any question related to programming language theory. I felt a little bad though, because a lot of the material went over everyone's head (it was a required course for CS majors).

He's also a certified pilot.

Re: λ Calculus (2013) [pdf]

#14
post #10

Earlier quoted context omitted.

The Y combinator is not the same as λ calculus. The Y combinator is an expression in λ calculus.

The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.

> which is what makes it a useful concept rather than an arbitrary bundle of rules.

I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.

Re: λ Calculus (2013) [pdf]

#15
post #10

Earlier quoted context omitted.

The Y combinator is not the same as λ calculus. The Y combinator is an expression in λ calculus.

The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.

The simply typed, and, especialy, the dependently typed lambda calculi are extremely versatile and powerful subsets of untyped lambda calculus which do not admit the Y combinator. Their usefulness does not at all require universality, and are, perhaps, more useful for being typed.

Re: λ Calculus (2013) [pdf]

#17

Can someone please explain to me why people always say THE lambda calculus?

How many do you want? If it's eponymous, it has a definite article. The positive integers, are quite distinct from all other sets.

Re: λ Calculus (2013) [pdf]

#18
post #15
post #10

Earlier quoted context omitted.

The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.

The simply typed, and, especialy, the dependently typed lambda calculi are extremely versatile and powerful subsets of untyped lambda calculus which do not admit the Y combinator. Their usefulness does not at all require universality, and are, perhaps, more useful for being typed.

There are many useful things that are not "the lambda calculus". "The lambda calculus" is more widely known and important, largely because it is universal, hence Church-Turing thesis.

Re: λ Calculus (2013) [pdf]

#19
post #10

Earlier quoted context omitted.

The Y combinator is in a sense the heart of the λ calculus; it's a key discovery for understanding that the λ calculus is universal, which is what makes it a useful concept rather than an arbitrary bundle of rules.

> which is what makes it a useful concept rather than an arbitrary bundle of rules. I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.

The lambda calculus was never meant to be a "practical FP language"; it predates programming languages and even mechanical stored-program computers as we understand them.

Re: λ Calculus (2013) [pdf]

#20
post #19

Earlier quoted context omitted.

> which is what makes it a useful concept rather than an arbitrary bundle of rules. I cannot recall a single practical FP language based on the Y combinator for recursion. The typical approach is to extend lambda calculus with a separate recursion primitive.

The lambda calculus was never meant to be a "practical FP language"; it predates programming languages and even mechanical stored-program computers as we understand them.

What are the useful cases of the Y combinator then? (I don't say that the lambda calculus is useless, I was responding to a comment that claimed the lambda calculus is useless without the Y combinator.)
Post reply on HN