5/14/2026 at 8:00:25 AM
The author presents most known numeral systems (ways of representing natural numbers) in lambda calculus, classified by whether the term use their bound variables exactly one time (linear), at most one time (affine), or multiple times (non-linear). Mackie's paper [0] (one of the references) provides a good introduction to these.He illustrates some numerals in each system with a graphical notation that strongly reminds me of interaction nets [1], a computational model closely related to lambda calculus. The notation they use for lambda terms is rather non-standard. Compare
> In β-reduction, k[(x⇒b)←a]⊳k[b{a/x}]k[(x⇒b)←a]⊳k[b{a/x}]
with Wikipedia's [2]
> The β-reduction rule states that a β-redex, an application of the form (λx. t) s, reduces to the term t[x:=s].
The k[...] part means that β-reduction steps can happen in arbitrary contexts.
[0] https://www.researchgate.net/publication/323000057_Linear_Nu...
by tromp