Lambda Calculus Interpreter

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

   λ s n.s (s (s (s (s (s n)))))

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

    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.