A reference catalog of lambda calculus numeral encodings across Linear (Mackie, Parigot), Affine (Scott, Bruijn), and Non-Linear (Church, Mogensen, Wadsworth) categories, each supporting arithmetic.
Key Takeaways
Seven distinct numeral systems are presented: Mackie, Parigot, Scott, Bruijn, Church, Mogensen, and Wadsworth, organized by variable usage discipline.
Linear encodings require each variable used exactly once; Affine allow unused variables; Non-Linear require explicit duplication nodes for reuse.
Mogensen’s encoding generalizes to arbitrary base b, enabling compact binary (b=2) or higher-base numerals with logarithmic term size.
Bruijn encoding (Borner 2026) represents n as x followed by n anonymous wildcard binders, giving a structurally minimal affine numeral.
Wadsworth numerals are the most structurally complex, threading a linked predecessor chain and applying each successor argument twice.
