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

51–60 of 73 posts

Re: λ Calculus (2013) [pdf]

#51

Post by teddyh »

lisper wrote: post #42
anyfoo wrote: post #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:…

You might enjoy this: https://flownet.com/ron/lambda-calculus.html

Or this: https://www.reddit.com/r/ProgrammerHumor/comments/uosex4/no_...>

Re: λ Calculus (2013) [pdf]

#52

Post by agumonkey »

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…

Does it mention a link between lambda and pi calculus (if any, i'm just wondering)

Re: λ Calculus (2013) [pdf]

#53

Post by agumonkey »

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

you could argue that Y is also an advanced CPS transform and a lot of patterns rely on similar idea, mainly passing the following computation as a functional parameter

Re: λ Calculus (2013) [pdf]

#54

Post by vcdimension »

There are several games and other online resources for learning lambda calculus and combinators:

For kids: http://worrydream.com/AlligatorEggs/ and: https://metatoys.org/alligator/

A lambda calculus calculator: https://lambster.dev/

A tetris style game for learning combinators: https://dirk.rave.org/combinatris/

Re: λ Calculus (2013) [pdf]

#55

Post by tromp »

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.e. a function f such that

    f |0| = True
    f |n+1| = False
Equivalently, we can ask if it's possible to convert these numerals to Church numerals, the standard number representation in lambda calculus. If one cannot, then these numerals don't seem to be useful in any way, and don't deserve to be called a number representation.

This reminds me of someone proposing to represent the number n in combinatory logic with basis {S,K} as simply S^n K, i.e. using K as Zero and S as Successor. That one does turn out to be convertible to Church numerals [1].

[1] https://john-tromp.medium.com/sk-numerals-9ad1b5634b28

Re: λ Calculus (2013) [pdf]

#56

Post by tromp »

vcdimension wrote: post #54

There are several games and other online resources for learning lambda calculus and combinators: For kids: http://worrydream.com/AlligatorEggs/ and: https://metatoys.org/alligator/ A lambda calculus calculator: https://lambster.dev/ A tetris style game for learning combinators: https://dirk.rave.org/combinatris/

The International Obfuscated C Code Contest also features a lambda calculus interpreter [0] with corresponding hint file [1].

[0] https://www.ioccc.org/2012/tromp/tromp.c

[1] https://www.ioccc.org/2012/tromp/hint.html

Re: λ Calculus (2013) [pdf]

#57

Post by librexpr »

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

The expansion into |n|(args...) must happen before we know what n is, because in the lambda calculus we can't know anything about a function without calling it. Since it happens before we know what n is, then the number of args will necessarily be the same for all n. When n > numargs, |n|(args...) ignores all its arguments and halts, and therefore f cannot be a useful test for zero.

Re: λ Calculus (2013) [pdf]

#58

Post by macartain »

vishnugupta wrote: post #45
chs20 wrote: post #39

What is the motivation for lambda calculus?

A little bit of historical background. There was a concerted effort in the late 19th, early 20th century (perhaps earlier too) to mechanise computation i.e., reducing it to a pure symbolic manipulation. There were obvious benefits, a famous one being Enigma Machine that was used to (successfully I think) break the German code during WW-2. On the philosophical side a parallel and overlapping effort was going on to fig…

ooh! phil wadler lectured me at glasgow.. he was always listenable but he's got funnier...

Re: λ Calculus (2013) [pdf]

#59

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…

Thanks; you confirmed my suspicion. This is not a useful number representation.

> When n > numargs, |n|(args...) ignores all its arguments and halts

I would say it reduces to a term of the form \_. \_. M that is definitely different from both False and True.

Post reply on HN