- A Brief History
- A Quick Primer for λ-Calculus
- Reduction Explained
- Church Numerals
- Pairs and Lists
x = 123So how do we arrive at a state of familiarity and clarity from a starting state of confusion? Let's dive in with some examples, and take it step at a time :-) Once we've got our heads wrapped around Alonzo Church's notation, we'll be able to easily read it -- and thus convert it into code! (We will have lots of practice in the coming posts to do just that.)
A Quick Primer for λ-Calculus
Here's one of the simplest definitions in λ-calculus that you're going to see: the identity function:
λx.xThis reads as "Here is a function that takes x as an argument and returns x." Let's do some more:
λxy.x"Here is a function that takes x and y as arguments and returns only x."
λx.λy.xy"An outer function takes x as an argument and an inner function takes y as an argument, returning the x and the y." Note that this is exactly equivalent to the following (by convention):
λxy.xyLet's up the ante with a function application:
λf.λx.f x"Here is a function that takes a function f as its argument; the inner function takes x as its argument; return the result of the function f when given the argument x." For example, if we pass a function f which returns its input multiplied by 2, and we supplied a value for x as 6, then we would see an output of 12.
Let's take that a little further:
λf.λx.f (f (f x))"Here is a function that takes a function f as its argument; the inner function takes x as its argument. Apply the function f to the argument x; take that result and apply f to it. Then do it a third time, returning that result." If we had the same function as the example above and passed the same value, our result this time would be 48 (i.e., 6 * 2 * 2 * 2).
That's most of what you need to read λ-calculus expressions. Next we'll take a peek into the murky waters of λ-calculus reduction and find that it's quite drinkable, that we were just being fooled by the shadows.