zlacker

>>tromp+(OP)
Meaningless question. If you allow arbitrary number formats you can just define 1 to be an arbitrarily large number.

>>IshKeb+db6
But the lambda calculus is far from an arbitrary format. It's about the oldest and least arbitrary formalism for computation.

>>tromp+ud6
Perhaps the lambda calculus proper is the oldest, but the choices made in encoding the binary lambda calculus are somewhat arbitrary: for instance, why use de Bruijn indices for symbols, instead of some other scheme, such as the index of the lambda in the string? And why encode de Bruijn indices in unary, and not in any other 1-prefixed self-delimiting format? And why use a self-delimiting format in the first place? Obviously, these choices are quite reasonable and make for a simple implementation, but they're totally distinct from the formalism that Church first described. (And for that matter, Church originally only used lambda notation in the context of an overarching logical formalism that later got struck down.)

Indeed, if we look at Church's paper, we'd find that the term is 80 symbols written fully, {λt[{{{{{t}(t)}(λh[λf[λn[{{{n}(h)}(f)}(n)]]])}(t)}(t)}(t)]}(λf[λx[{f}({f}(x))]]), or 44 symbols when abbreviated, {λt t(t, (λh λf λn n(h, f, n)), t, t, t)}(λf λx f(f(x))), which aren't too impressive given the alphabet of 11 or 12 symbols.

>>Legion+rx6
> but the choices made in encoding the binary lambda calculus are somewhat arbitrary

I made the simplest choices I could that do not waste bits.

> And why use a self-delimiting format in the first place?

Because a lambda term description has many different parts that you need to be able to separate from each other.

> And why encode de Bruijn indices in unary

I tried to answer that in more detail in this previous discussion [1].

[1] >>37584869