4 ms·
The number representation proposed by the author is one I've never seen before: |0| = λx. x |n+1| = λ_. |n| In other words, 0 is identity, and succe
by tromp 3y ago
The number representation proposed by the author is one I've never seen before:
|0| = λx. x
|n+1| = λ_. |n|
In other words, 0 is identity, and successor is the const function. This makes the predecessor function easy to define. Just apply Succ n to anything to get n back. The article fails to answer the most crucial question about these numerals though:
Can we write a function that tests if a numeral represents 0?
I.e. a function f such that
f |0| = True
f |n+1| = False
Equivalently, we can ask if it's possible to convert these numerals to Church numerals, the standard number representation in lambda calculus.
If one cannot, then these numerals don't seem to be useful in any way, and don't deserve to be called a number representation.
This reminds me of someone proposing to represent the number n in combinatory logic with basis {S,K} as simply S^n K, i.e. using K as Zero and S as Successor. That one does turn out to be convertible to Church numerals [1].
[1] https://john-tromp.medium.com/sk-numerals-9ad1b5634b28 https://john-tromp.medium.com/sk-numerals-9ad1b5634b28
- librexpr 3y agoI'm pretty sure it's impossible to write a function that tests for zero for these numerals. Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) with some number of args. This call must be toplevel, not as an argument to another function, because otherwise it is lazy and not executed. The number of args also cannot be infinite, since that would require an infinitely large program. The expansion into |n|(args...) must happen before we know what n is, because in the lambda calculus we can't know anything about a function without calling it. Since it happens before we know what n is, then the number of args will necessarily be the same for all n. When n > numargs, |n|(args...) ignores all its arguments and halts, and therefore f cannot be a useful test for zero.
- tromp 3y agoThanks; you confirmed my suspicion. This is not a useful number representation. > When n > numargs, |n|(args...) ignores all its arguments and halts I would say it reduces to a term of the form \_. \_. M that is definitely different from both False and True.
- tromp 3y ago> Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) Actually, this is not true. f |n| could expand into \x. \y. (|n| args...) instead, where the args contain x and y. But the rest of your argument still applies to the application of |n|.
- librexpr 3y agoYou're right, that was imprecise of me. But if F = (\x. \y. (|n| args...)) is equivalent to True or False, then it is also equivalent to (F True False), which brings us back to a toplevel (|n| args...). Another slight correction/expansion is that (|n| args...) = n - numargs when n >= numargs. This happens to coincide with False when n = numargs + 1, so it would have been better if I had said "when n > numargs + 1".
- 9bf770f3 3y agoIt is interesting that in the linked document exercises 4 and 10 ask you to implement addition for those kinds of numerals. Can you think of a way doing this without checking for zero? (I know that sometimes there are unsolvable exercises in the literature, but the author gives this routinely as an assignment it seems [1].) [1] http://wcl.cs.rpi.edu/pdcs/slides/Chapter2-LambdaCalculus.ppt http://wcl.cs.rpi.edu/pdcs/slides/Chapter2-LambdaCalculus.pp...
- tromp 3y agoI sent an email to the professor that taught the course in 2011 asking for clarification...