Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

λ Calculus (2013) [pdf]

cs.rpi.edu

Post reply on HN
Print view View original

31–40 of 73 posts

Re: λ Calculus (2013) [pdf]

#31

Post by kragen »

Hirrolot wrote: post #20
lmm wrote: post #19

Earlier quoted context omitted.

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

the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all

so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it

if you can't, you may have gained enough insight into the problem to show that the system actually does guarantee termination, and maybe even show useful time bounds on it

if you can, you have usually shown the system is turing-complete, which means you can appeal to rice's theorem whenever you are tempted to analyze the behavior of the system in any way, so you can satisfy yourself with partial decision procedures that work often enough to be useful and are conservative in the appropriate way, rather than wasting time trying to find a complete solution

(also if you're designing the system you might consider either supporting iteration more directly or removing the back door)

every once in a while it's also useful in practice to be able to program a weird machine, too

Re: λ Calculus (2013) [pdf]

#32

Post by Hirrolot »

lmm wrote: post #27
Hirrolot wrote: post #20

Earlier quoted context omitted.

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

Emulating recursion, and more generally the whole Church-Turing thesis. The fact that you can represent mechanical computation through, well, computation - the fact that equating those concepts makes sense at all, which was such a huge innovation that today it seems too banal to even notice.

You keep answering with the same words though. My question was _where_ the Y combinator is useful, not _what_ it is designed for, which I am of course aware of.

Re: λ Calculus (2013) [pdf]

#33

Post by throwawaylinux »

photochemsyn wrote: post #23
carlineng wrote: post #7

My favorite discussion of this topic is from David Beazley: https://www.youtube.com/watch?v=5C6sv7-eTKg He does a wonderful job of taking very dense mathematical notation and explaining it in ways that anyone can understand. He derives the basic concepts of the lambda calculus from the ground up using Python. Super fun to follow along with.

That looks interesting, although it is 3 hrs. I like this ~45 minute intro to the concept, which seems a little more Turing-accesible:, in that it shows how you can implement addition and multiplication in the system, which is a lot: https://youtu.be/OLH3L285EiY successor function: given a number, get the next number try this in Python: zero = lambda f: lambda x: x one = lambda f: lambda x: f(x) two = lambda f: lambd…

What's Turing-accesible?

Re: λ Calculus (2013) [pdf]

#34

Post by Hirrolot »

kragen wrote: post #31
Hirrolot wrote: post #20

Earlier quoted context omitted.

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

the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it if you can't, you may have ga…

> the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all

This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice?

The Y combinator as a counterexample of termination is a great insight though!

Re: λ Calculus (2013) [pdf]

#35

Post by kragen »

Hirrolot wrote: post #34
kragen wrote: post #31

Earlier quoted context omitted.

the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it if you can't, you may have ga…

> the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice? The Y combina…

typing is often an excellent way to ensure termination

Re: λ Calculus (2013) [pdf]

#36

Post by craftuser »

irascibeth wrote: post #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 the…

+1 from another RPI alum. One of my big regrets from college is missing out on doing undergrad research with him. https://www.cs.rpi.edu/~cvarela/research.html

Re: λ Calculus (2013) [pdf]

#38

Post by fanf2 »

Hirrolot wrote: post #14
lmm wrote: 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 Miranda programming language was an early lazy functional programming language, an ancestor of Haskell. It compiles down to combinators, and uses combinator reduction as its evaluation strategy. This became obsolete by the end of the 1980s but it’s still neat to learn how it works. One of the primitive combinators is Y. Here is its implementation: https://github.com/pkreyenhop/miranda/blob/master/reduce.c#L...

Re: λ Calculus (2013) [pdf]

#40

Post by fanf2 »

Hirrolot wrote: post #34
kragen wrote: post #31

Earlier quoted context omitted.

the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all so when you're faced with a formal system that doesn't seem to support indefinite iteration, perhaps because you are trying to design it to guarantee termination, a useful exercise is to try to construct an analogue of the y-combinator in it if you can't, you may have ga…

> the great benefit of the y-combinator is that it permits indefinite iteration in a system that seems at first glance to not support iteration at all This is only the case for untyped systems. If we try to type the Y combinator, we will eventually need some notion of recursion. For example, in Haskell/OCaml we can type it with iso/equi-recursive types. How many truly untyped systems we use in practice? The Y combina…

Dynamically typed programming languages are statically untyped.

You might argue they are unityped, but that’s really a type theoretician’s job security: if a language has the untyped lambda calculus as a subset (like the python example in this discussion) it’s reasonable to call it untyped.

Post reply on HN