De Bruijn Numerals
6 days ago
- #de-bruijn-indices
- #lambda-calculus
- #numeral-systems
- Introduction of a novel encoding method called 'de Bruijn numerals' using nested de Bruijn indices.
- Explanation of the encoding with an example: the decimal number 4 is encoded as λ54.
- Reference to Wadsworth's (1980) work on numeral systems and the concept of 'adequate' numeral systems.
- Discussion on the limitations of de Bruijn numerals, particularly the absence of a zero? function.
- Presentation of arithmetic operations (succ, pred, add) with proofs using β-reduction.
- Introduction of hybrid implementations combining de Bruijn numerals with Church numerals for operations like multiplication and factorial.
- Application of de Bruijn numerals in solving practical problems, such as projections in Church n-tuples.
- Description of functions for manipulating Church n-tuples, including selector, push, pop, and move.
- Conclusion with an invitation for feedback and further exploration of de Bruijn numerals.