This is a great introduction to that most ancient and elegant model of computation. But I was a little sad to read: > One can represent natural numbers in a si

This is a great introduction to that most ancient and elegant model of computation. But I was a little sad to read: > One can represent natural numbers in a simple way, as follows: > Definition (ordered tuples, natural numbers) The ordered tuple ⟨a0 , … an⟩ of λ-terms is defined as λx [x a0 … an]. One then defines the λ -term ┌ n ┐ corresponding to the natural number n as: ┌ 0 ┐ = I and, for every k, ┌ k + 1 ┐ = ⟨F, ┌ k ┐⟩ which is a rather convoluted and impractical way to represent natural numbers compared to the Church numerals Cn which iterate a given function n times on a giving argument. There are cases where it makes sense to use tuples to represent natural numbers, namely to simplify the definition of predecessor, subtraction, and comparison. But that uses 1-tuples rather than 2-tuples [1]. Replacing Church numerals by tuple numerals allowed a googologically VERY large number (based on the so-called Bashicu Matrix System) to be expressed in only 350 bits rather than 404 bits. [2] [1] https://github.com/tromp/AIT/blob/master/numerals/tuple_numerals.lam https://github.com/tromp/AIT/blob/master/numerals/tuple_nume... [2] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/bms.lam https://github.com/tromp/AIT/blob/master/fast_growing_and_co...