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

61–70 of 73 posts

Re: λ Calculus (2013) [pdf]

#61

Post by HWR_14 »

pingohits wrote: post #13
leetrout wrote: post #4

Earlier quoted context omitted.

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.

I wonder why so many very technical people are pilots.

Re: λ Calculus (2013) [pdf]

#62

Post by tromp »

commandlinefan wrote: post #60

> f(x) = x^2, f : Z → Z Shouldn't that be: f(x) = x^2, f : Z → Z+ ?

No, the type annotation merely specifies that the codomain of f is Z. It's not intended to specify the range of the function.

Z+ is not the range of this f either; it is Z^{>=0}.

Re: λ Calculus (2013) [pdf]

#64

Post by leetrout »

HWR_14 wrote: post #61
pingohits wrote: post #13

Earlier quoted context omitted.

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.

I wonder why so many very technical people are pilots.

As a 100 hour, thrice restarted student pilot it is the perfect mix of physical, mental, math and procedures. The actual flying of small aircraft is physical coordination and task saturation at times. Lots of procedures and optimizations. The navigation, especially the dying radio navigation (with paper charts, too) and flight calculators is lots of geography and math and tools.

Drumming is some of that but other than motorcycles I've not found anything else that comes close to flying. I've never tried sailing but maybe that too?

Re: λ Calculus (2013) [pdf]

#65

Post by jjtheblunt »

ggm wrote: post #29
jjtheblunt wrote: post #21

Earlier quoted context omitted.

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.

It's quite funny. In the Big Ten unversities (american midwest) it's too late for Ohio State to undo the ongoing humor of "THE Ohio State" because everyone already for decades mocks it as funny and won't let it go.

Re: λ Calculus (2013) [pdf]

#68

Post by cubefox »

chewxy wrote: post #25
noman-land wrote: post #16

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

There are many lambda calculi. THE lambda calculus refers to the original lambda calculus as defined by Church.

Simply typed lambda calculus? Untyped lambda calculus?

Re: λ Calculus (2013) [pdf]

#69

Post by 9bf770f3 »

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

Re: λ Calculus (2013) [pdf]

#70

Post by tromp »

librexpr wrote: post #57
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.…

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

Post reply on HN