Live data from Hacker News

λ Calculus (2013) [pdf]

cs.rpi.edu

21–30 of 73 posts

Re: λ Calculus (2013) [pdf]

#21
post #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.

That reminds me of “THE Ohio State University”, contrasting with other Big Ten schools and their common names (Illinois, Indiana, Iowa, Northwestern, Purdue,…) where the THE is often laughed about as hust funny for the reason you cite.

Re: λ Calculus (2013) [pdf]

#22

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.

Thanks for sharing. He makes the material very interesting and very accessible. I've fallen into another HN rabbithole..

Re: λ Calculus (2013) [pdf]

#23

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: lambda x: f(f(x))

to_int = lambda n: n(lambda i: i+1)(0)

succ = lambda n: lambda f: lambda x: f(n(f)(x))

three = succ(two)

four = succ(three)

to_int(four)

So that's just counting, the Church Numerals, where it begins.

Re: λ Calculus (2013) [pdf]

#24
post #18
post #15

Earlier quoted context omitted.

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.

Of course there are other useful things. But a comment argued that the presence of Y is what makes untyped lambda calculus useful. My rebuttal is that certain subsets which (intentionally) lack Y are more useful. Applications of typed calculi abound, but one rarely sees applications of the untyped calculus. Universality is not so important, it would seem. For example, infinite computations can still be modeled in typed calculi, but one has more control over them in that setting than running on "bare metal" untyped lambda calculus.

Re: λ Calculus (2013) [pdf]

#26
post #24
post #18

Earlier quoted context omitted.

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.

Of course there are other useful things. But a comment argued that the presence of Y is what makes untyped lambda calculus useful. My rebuttal is that certain subsets which (intentionally) lack Y are more useful. Applications of typed calculi abound, but one rarely sees applications of the untyped calculus. Universality is not so important, it would seem. For example, infinite computations can still be modeled in typ…

Ok, "useless" is a slight exaggeration; non-universal calculi can be useful. But the thing that makes the lambda calculus so important and famous - the thing that makes it "the lambda calculus - is universality, and that's the ur-application that makes all of the subsequent application of calculi to mechanical computation possible.

Re: λ Calculus (2013) [pdf]

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

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.

Re: λ Calculus (2013) [pdf]

#28
In university, I had fun actually applying lambda calculus. Here’s a very silly python script.

    # a factorial function written entirely with just single-argumented lambdas
    # and calls
    fac = ((lambda p: p(p)(lambda q: lambda n: ((n(lambda e: lambda e:
      lambda a: a)(lambda i: lambda l: i))(lambda d: lambda c: c)
      (lambda m: (lambda m: lambda z: m(n(z)))(q(m)))((lambda c: lambda x:
      n(lambda g: lambda h: h(g(c)))(lambda u: x)(lambda u: u))))))
      (lambda s: lambda q: lambda w: q(s(s)(q))(w)))


    # for converting between church numerals and python numbers (you need
    # a few python functions and operators to manipulate them)
    natural = lambda c: c(lambda x: x+1)(0)
    church = lambda n: reduce(lambda x,y:
  (lambda n: lambda f: lambda x: f(n(f)(x)))(x), range(n), lambda f: lambda x: x)


    # test!
    # fac(10) is about the highest number computing in a few seconds on a core 2 CPU
    print natural(fac(church(10)))

Re: λ Calculus (2013) [pdf]

#29
post #17

Earlier quoted context omitted.

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

That reminds me of “THE Ohio State University”, contrasting with other Big Ten schools and their common names (Illinois, Indiana, Iowa, Northwestern, Purdue,…) where the THE is often laughed about as hust funny for the reason you cite.

Yes, I went to THE university of York. How dare the other one have the temerity to think it was THE university of York. No no, it's a jumped up teacher training college of Ripon and York St John, made university, just A university of York, not THE.

Also, York University in Canada confused things.

Re: λ Calculus (2013) [pdf]

#30
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.

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

[deleted]
Post reply on HN