Comment by jagthebeetle

Looking at https://text.marvinborner.de/2023-04-06-01.html helped me understand the syntax a bit (though I'm just a non-theoretical programmer).

I was confused about what <4> = \lambda ^ 5 4 meant, since it already seemed to have a "4" in it.

The trick is that the 4 seems to be similar to a positional argument index, but numbered inside out.

IOW, in this encoding, <4> is a function that can be called 5 times (the exponent on the lambda) and upon the fifth call will resolve to whatever was passed in 1st (which because of the inside-out ordering is labeled "4").

(For a simpler example, 0 is a function that can be called once and returns its argument.)

So succ is 3-ary; it says, give me a function (index 2, outermost call); next, give me its first argument (index 1, second-outermost call); when you call that (index 0, dropped, innermost call), I'll apply the function to the argument.

But note that if index 2 is a numeral <N>, the outermost call returns a function that will "remember" the next thing passed in and return it after 1 (succ's innermost call) + N + 1 (<N>'s contract) calls.