λ Calculus (2013) [pdf] • Hacker News Board

Re: λ Calculus (2013) [pdf]

#71

Post by tromp » Sun, Aug 20, 2023, 9:33 AM UTC

9bf770f3 wrote: post #69

tromp wrote: post #55

The number representation proposed by the author is one I've never seen before: |0| = λx. x |n+1| = λ_. |n| In other words, 0 is identity, and successor is the const function. This makes the predecessor function easy to define. Just apply Succ n to anything to get n back. The article fails to answer the most crucial question about these numerals though: Can we write a function that tests if a numeral represents 0? I.…

It is interesting that in the linked document exercises 4 and 10 ask you to implement addition for those kinds of numerals. Can you think of a way doing this without checking for zero? (I know that sometimes there are unsolvable exercises in the literature, but the author gives this routinely as an assignment it seems [1].) [1] http://wcl.cs.rpi.edu/pdcs/slides/Chapter2-LambdaCalculus.pp...

I sent an email to the professor that taught the course in 2011 asking for clarification...

Re: λ Calculus (2013) [pdf]

#72

Post by librexpr » Sun, Aug 20, 2023, 10:55 AM UTC

tromp wrote: post #70

librexpr wrote: post #57

Earlier quoted context omitted.

I'm pretty sure it's impossible to write a function that tests for zero for these numerals. Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) with some number of args. This call must be toplevel, not as an argument to another function, because otherwise it is lazy and not executed. The number of args also cannot be infinite, since that would require an infinitely la…

> Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) Actually, this is not true. f |n| could expand into \x. \y. (|n| args...) instead, where the args contain x and y. But the rest of your argument still applies to the application of |n|.

You're right, that was imprecise of me. But if F = (\x. \y. (|n| args...)) is equivalent to True or False, then it is also equivalent to (F True False), which brings us back to a toplevel (|n| args...).

Another slight correction/expansion is that (|n| args...) = n - numargs when n >= numargs. This happens to coincide with False when n = numargs + 1, so it would have been better if I had said "when n > numargs + 1".

Re: λ Calculus (2013) [pdf]

#73

Post by johnmw » Sun, Aug 20, 2023, 1:17 PM UTC

johnmw wrote: post #47

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.

This is another excellent video if you are more of a Javascript developer: https://www.youtube.com/watch?v=OLH3L285EiY

(Sorry, I actually meant to post this video: https://www.youtube.com/watch?v=3VQ382QG-y4)