Hacker News new | ask | show | jobs
by siraben 728 days ago
Yeah it terminates.

A tiny 63 bit program[0] in this language represents a number unfathomably larger than not only ack(9,9), but the far larger Graham’s Number as well. It originates in a Code Golf challenge asking for the “Shortest terminating program whose output size exceeds Graham’s number”, answered by user Patcail and further optimized by user 2014MELO03. With one final optimization applied.

Here's a really short program. Let's calculate 2 * 3

  (λn m s. n (m s)) (λf n. f (f n)) (λf n. f (f (f n)))
eventually it terminates with

   λ s n.s (s (s (s (s (s n)))))
which is just the church encoding of 6.

[0] https://tromp.github.io/blog/2023/11/24/largest-number

3 comments

A even smaller 49-bit program whose normal form size also exceeds Graham’s Number was found more recently:

    (λJ.J J) (λy.y (y (λg.λm.m g (λf.λx.f (f x)))))
[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_co...
Thanks. A page with examples would be really helpful. The default example (if that what it is) or the shared example would be much more interesting with some context. Or a Show HN, if that’s what’s happening here.
The default page, without including a term does have some explanation

https://lambda-calculus-interpreter.netlify.app/

Patcail made a web game in that theme as well: https://patcailmemer.github.io/Ordinal-Markup/