Some numbery functions
Somewhat a test-post, for to have not dead lambda calculus within post.
(There’s also kind of a lambda playground over here.)
To try, put cursor on line below and do like ctrl+enter couple of times:
If it works (if the ctrl+enter-business leads to a line that goes foo bar), we can make like, a few numbers... (ctrl+enter each line).
(Oh by the way. Can do ctrl+l to insert a λ, and ctrl+d to insert a ≜. Or can use \ instead of λ and := instead of ≜.)
The idea, or at least one way to look at it, is that the number five is the function that does something five times. So, if we want to foo a bar five times, then we can... (ctrl+r to replace 5 with the lambdas from the definition we did above. Then ctrl+enter a couple of times.)
Which quite possibly evaluated to foo (foo (foo (foo (foo bar)))). Which is like five foos.
Okay. Addition is pretty numbery let’s that. Below is a function that takes arguments a and b. And gives back, uh, a λf.λx.-function. This function applies f “b times” to x, and applies f “a times” to the result of that again. Hopefully amounts to like, an a + b number of fs applied to x. (ctrl+enter on line below)
If things seem fine so far, we can try to use it to like, actually additioning. ctrl+r on line below to replace the names of the things we’ve defined with their lambdas. Then ctrl+enter a bunch of times to evaluate. (Or ctrl+shift+enter one time.)
It’s maybe twelve! (Hopefully.)