31 Oct 2018
3 min read
I've long since heard of "Lambda Calculus" but I didn't really know what it is about until I saw this video. It got me super excited! What I love about it is that it's built on almost nothing! Only the concept of functions. It's so simple and elegant! Professor Graham Hutton also listed good reasons to learn it:
-Lambda calculus can encode any computation, and any programming language can be encoded in lambda calculus. (I will explain what "encoding" is below.) -It is the basis for functional programming languages, including Haskell and OCaml. -Most major programming languages include it as a major component.
Since it's so simple yet powerful, I must learn it to be a better programmer!
Lambda Calculus builds on the concept of functions. A function takes in input(s), processes the input(s) and returns an output. E.g., a function can take an input x, and output x+1. Or, a function can take inputs x and y, and output x+y. In lambda calculus, we write these functions as
An input is followed by a λ, a dot separates each input, and the last dot is followed by the output of the function. We evaluate a function in the usual manner. In terms of notation, we write the value(s) of the input(s) after we define the function. E.g., when x = 5 in the first function above, we write:
(λx.x+1) 5 = 5 + 1 = 6
Or, when x = 5 and y = 7 in the second function, we write:
(λx.λy.x+y) 5 7 = 5 + 7 = 12
Of course, we can name a function. Doing so let us encode functions and operators. We name/encode TRUE as the function that returns the first input of a function that takes two inputs:
TRUE = λx.λy.x
And FALSE is the function that returns the second input of a function that takes two inputs:
FALSE = λx.λy.y
Using the functions TRUE and FALSE, we can encode the logical operator NOT, which takes a boolean (i.e., TRUE or FALSE) and returns the opposite:
NOT = λb.b FALSE TRUE
We read the notation above as: the NOT function takes a b (stands for boolean) as an input, and the output is applying b to the inputs FALSE TRUE.
We can verify that NOT does what it's supposed to do by evaluating the result of NOT when it's given FALSE as the input:
= (λb. b FALSE TRUE) FALSE (substitute in the definition of NOT)
= FALSE FALSE TRUE (FALSE is the input to NOT, so it's to be applied to FALSE TRUE)
= TRUE (Applying the function FALSE means returning the second input, i.e., TRUE)
NOT FALSE returns TRUE, as we expected. (See the video for the evaluation of NOT TRUE)
Professor Hutton gave us the exercise of constructing the AND and OR operators. Here is my attempt:
AND = λb1.λb2.b1 b2 FALSE
AND takes two boolean inputs, then applied the first input (which is a function of either TRUE or FALSE) to the second input and FALSE.
How did I get this? I know that AND takes in two booleans, so the first part (λb1.λb2) is easy. The AND operator needs to return a boolean (TRUE only when both inputs are TRUE, otherwise, FALSE). So I know that it should take FALSE as an input, because I want it to be able to return FALSE even when there is some TRUE. Also, I know I have to consider both inputs so one of the input has to be applied to the function. So, I applied b1 (i.e., either the function TRUE or FALSE) to the inputs b2 and FALSE.
I've verified that AND behaves correctly in all cases:
AND TRUE TRUE = (λb1.λb2.b1 b2 FALSE) TRUE TRUE = TRUE TRUE FALSE = TRUE AND TRUE FALSE = (λb1.λb2.b1 b2 FALSE) TRUE FALSE = TRUE FALSE FALSE = FALSE AND FALSE TRUE = (λb1.λb2.b1 b2 FALSE) FALSE TRUE = FALSE TRUE FALSE = FALSE AND FALSE FALSE = (λb1.λb2.b1 b2 FALSE) FALSE FALSE = FALSE FALSE FALSE = FALSE
The OR operator is obviously analogous to the AND operator in many ways. Here is my first attempt:
OR = λb1.λb2.b1 b2 TRUE
OR returns FALSE only when both of the inputs are FALSE, otherwise, it returns TRUE. I verify that my encoding of OR behaves correctly by checking each case:
OR TRUE TRUE = (λb1.λb2.b1 b2 TRUE) TRUE TRUE = TRUE TRUE TRUE = TRUE (Yes!) OR TRUE FALSE = (λb1.λb2.b1 b2 TRUE) TRUE FALSE = TRUE FALSE TRUE = FALSE (Oh no! But if it's b1 b1 b2, then it'd work.) OR FALSE TRUE = (λb1.λb2.b1 b2 TRUE) FALSE TRUE = FALSE TRUE TRUE = TRUE (Yes!) OR FALSE FALSE = (λb1.λb2.b1 b2 TRUE) FALSE FALSE = FALSE FALSE TRUE = TRUE (Oh no! But if it's b1 b1 b2, then it'd work.)
So it doesn't work. But for the cases that wouldn't work, I noticed another encoding that would work:
OR = λb1.λb2.b1 b1 b2
As you can see, applying this encoding to cases 1 and 3 above still work. Therefore, the encoding works in all cases. I changed it to this encoding because I noticed that I need more elements of an input rather than a fixed TRUE as the last input.
I hope by now you see why I love Lambda Calculus! In the next post, I'll talk about the magical function that lets you do recursion: the Y combinator.
Software engineer. Loves FP Haskell Coq Agda PLT. Always learning. Prior: Economist. Vegan, WOC in solidarity with POC.
See other articles by Marty
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!