Some numbery functions


This post is part of a list: Some lambda-notes
Next thing: How do the lambdas?

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:

(λx.λy.y x) bar foo

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 .)

0 ≜ λf.λx.x 1 ≜ λf.λx.f x 2 ≜ λf.λx.f (f x) 5 ≜ λf.λx.f (f (f (f (f x))))

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.)

5 foo bar

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 fb times” to x, and applies fa 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)

+ ≜ λa.λb.λf.λx.a f (b f x)

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.)

+ 5 (+ 5 2)

It’s maybe twelve! (Hopefully.)