Lambda Calculus Interpreter
lambda-calculus-interpreter.netlify.appSource code may be found at https://github.com/ascandone/elm-lambda-interpreter
It seems to scroll forever. Does this example terminate? What would be an easier example to try?
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
eventually it terminates with(λn m s. n (m s)) (λf n. f (f n)) (λf n. f (f (f n)))
which is just the church encoding of 6.λ s n.s (s (s (s (s (s n)))))A even smaller 49-bit program whose normal form size also exceeds Graham’s Number was found more recently:
[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_co...(λJ.J J) (λy.y (y (λg.λm.m g (λf.λx.f (f x)))))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
Patcail made a web game in that theme as well: https://patcailmemer.github.io/Ordinal-Markup/
let Sub = λ a b f c.b (\ x.x True) (a (\ cc o.o cc (f (cc False))) (λ o.o c c)) False
Extending the subtraction to the bigints represented as little-endian lists of bytes is left as an exercise to the reader.let True = t f. t let False = t f. f let not = x. x False True let Byte = b7 b6 b5 b4 b3 b2 b1 b0. f. f b7 b6 b5 b4 b3 b2 b1 b0 let xor3 = a b c. a (b c (not c)) (b (not c) c) let maj3 = a b c. a (b True c) (b c False) let full_adder = a b c k. k (xor3 a b c) (maj3 a b c) let adc = a b ci k. a (b ( b7 b6 b5 b4 b3 b2 b1 b0. ( a7 a6 a5 a4 a3 a2 a1 a0. ( full_adder a0 b0 ci (s0 c0. full_adder a1 b1 c0 (s1 c1. full_adder a2 b2 c1 (s2 c2. full_adder a3 b3 c2 (s3 c3. full_adder a4 b4 c3 (s4 c4. full_adder a5 b5 c4 (s5 c5. full_adder a6 b6 c5 (s6 c6. full_adder a7 b7 c6 (s7 c7. k (Byte s7 s6 s5 s4 s3 s2 s1 s0) c7 )))))))))))) let inv = b. b (b7 b6 b5 b4 b3 b2 b1 b0. Byte (not b7) (not b6) (not b5) (not b4) (not b3) (not b2) (not b1) (not b0)) let sub = a b. adc a (inv b) True (s _. s) let Zero = z i. z let Int = lsb rest. z i. i (lsb rest)P.S. De we really need a leading \ or λ for the lambda-abstraction? I personally think the dot is quite unambiguous and clear on its own.
so easy to read, missed a comma in line 503