~ back to blog

Lambda calculus 1

Let’s get started with some funny things. If we have a function f(x) = x + 1, it could be described in lambda calculus as λx.x+1.

Something more interesting could be a function accepting two parameters x and y, and returning the sum of the squares of each parameter. Semantically, we could express the idea like so: f(x, y) = x^2 + y^2. In lambda calculus, we can write it like this: λx.λy.x^2+y^2.

Note that instead of one function call we make two calls to a lambda and pass one parameter each, that’s because each lambda function can only accept one argument at a time.

I am going to have a bit of fun, if you allow me, and I am going to rewrite some algebraic functions as lambda expressions:

  1. x - y + 2z, then λx.λy.λz.x - y + 2z
  2. -x + 5, then λx.- x + 5
  3. a^2+b^2-c^2, then λa.λb.λc.a^2 + b^2 + c^2
  4. t^2 - π, then λt.t^2 - π

Let’s perform a substitution in the formula λx.x + 1. If we were to plug in a specific value for x, we would perform a substitution and it would be expressed like so: (λx.x + 1) 92, which we could evaluate to be 92 + 1 = 93.

Now that we have handled the arithmetic operations, let’s move on to other fundamental values/properties in programming. Let’s start with TRUE, FALSE (aka boolean-type values). Can we represent them in lambda calculus?

We have a few things we can do in lambda calculus:

  1. use variables
  2. use lambda expressions
  3. get output from the function (aka lambda expression)

We can represent each and every data type with these properties. When it comes to boolean values, we are essentially making a choice from two elements, we either pick TRUE or we pick FALSE. So we are going to encode this choice by taking two variables x and y and we shall apply the logic like so: 

TRUE = λx.λy.x
FALSE = λx.λy.y

If we pick x, we shall consider the value to be TRUE. If we pick y, we shall consider the value to be FALSE. We have now made this abstraction around boolean values, but we could likely use it for any binary choice, such as picking an element from enum team {red, blue}.

With logical values defined, we can start defining logical operations in the lambda calculus. One could think of many logical operations possible, we shall stick with NOT for now, because it’s the simplest logical operation (the only one that is unary, at least to my knowledge) and try to define it in the lambda calculus. 

NOT = λx.x FALSE TRUE

Well, this came out of nowhere, didn’t it? Let’s examine the thought process - since NOT is a unary operation, we assume it only takes one argument, one parameter, so we define only one lambda expression.

Let’s see if this NOT operation of ours works. Since we are working with boolean values, we can prove it easily be exhausting all possible values (TRUE, FALSE) in the domain and substituting for them in the expression. So we take the entire expression and perform a substitution. We assume the result to be the opposite truth value for each boolean, so TRUE if we substitute with FALSE and vice versa. 

(λx.x FALSE TRUE) FALSE = FALSE FALSE TRUE = λx.λy.y FALSE TRUE = (λx.λy.y) FALSE TRUE = TRUE

As can be seen, the substitution worked. Reader might as well try it for TRUE to make sure they get FALSE.

Let’s do something more interesting together! How about we define AND operation in lambda calculus?

We know since AND is a binary operation, we shall probably be using two variables with some constants to arrive at our derived value. Let us create a triplet of values constructed out of our variables. Remember, the formula may not be only true if both x and y are true at the same time. Starting at our first attempt: 

(λx.λy.xxx) TRUE TRUE = TRUE TRUE TRUE = (λx.λy.x) TRUE TRUE = TRUE
(λx.λy.xxx) TRUE FALSE = TRUE TRUE TRUE = (λx.λy.x) TRUE TRUE = TRUE
(λx.λy.xxx) FALSE TRUE = FALSE FALSE FALSE = (λx.λy.y) FALSE FALSE = FALSE
(λx.λy.xxx) FALSE FALSE = FALSE FALSE FALSE = (λx.λy.y) FALSE FALSE = FALSE

We have actually got truth values corresponding to the truth value of x, but that isn’t what we’re after, let’s create a triplet where we introduce y: 

(λx.λy.xxy) TRUE TRUE = TRUE TRUE TRUE = (λx.λy.x) TRUE TRUE = TRUE
(λx.λy.xxy) TRUE FALSE = TRUE TRUE FALSE = (λx.λy.x) TRUE FALSE = TRUE

This did not seem to work out, we already got TRUE for values of TRUE and FALSE. Let’s shift y to the left. 

(λx.λy.xyx) TRUE TRUE = TRUE TRUE TRUE = (λx.λy.x) TRUE TRUE = TRUE
(λx.λy.xyx) TRUE FALSE = TRUE FALSE TRUE = (λx.λy.x) FALSE TRUE = FALSE
(λx.λy.xyx) FALSE TRUE = FALSE TRUE FALSE = (λx.λy.y) TRUE FALSE = FALSE
(λx.λy.xyx) FALSE FALSE = FALSE FALSE FALSE = (λx.λy.y) FALSE FALSE = FALSE
AND = λx.λy.xyx

It seems we have found an expression for AND operation!

Let’s have more fun, and try OR:

(λx.λy.xxy) TRUE TRUE = TRUE TRUE TRUE = (λx.λy.x) TRUE TRUE = TRUE
(λx.λy.xxy) TRUE FALSE = TRUE TRUE FALSE = (λx.λy.x) TRUE FALSE = TRUE
(λx.λy.xxy) FALSE TRUE = FALSE FALSE TRUE = (λx.λy.y) FALSE TRUE = TRUE
(λx.λy.xxy) FALSE FALSE = FALSE FALSE FALSE = (λx.λy.y) FALSE FALSE = FALSE
OR = λx.λy.xxy

Success! It seems like we could use a challenge, eh? Let’s try XOR! 

(NOT λx.λy.xy FALSE) TRUE TRUE = NOT TRUE TRUE FALSE = (λx.x FALSE TRUE) TRUE TRUE FALSE = TRUE FALSE TRUE TRUE FALSE = (λx.λy.x FALSE TRUE) TRUE FALSE = TRUE FALSE TRUE = (λx.λy.x) FALSE TRUE = FALSE
(NOT λx.λy.xy FALSE) TRUE FALSE = NOT TRUE FALSE FALSE = (λx.x FALSE TRUE) TRUE FALSE FALSE = TRUE FALSE TRUE FALSE FALSE = (λx.λy.x FALSE TRUE) FALSE TRUE = FALSE FALSE TRUE = (λx.λy.y) FALSE TRUE = TRUE
(NOT λx.λy.xy FALSE) FALSE TRUE = NOT FALSE TRUE FALSE = (λx.x FALSE TRUE) FALSE TRUE FALSE = FALSE FALSE TRUE TRUE FALSE = (λx.λy.y FALSE TRUE) TRUE FALSE = TRUE TRUE FALSE = (λx.λy.x) TRUE FALSE = TRUE
(NOT λx.λy.xy FALSE) FALSE FALSE = NOT FALSE FALSE FALSE = (λx.x FALSE TRUE) FALSE FALSE FALSE = FALSE FALSE TRUE FALSE FALSE = (λx.λy.y) FALSE TRUE FALSE FALSE = TRUE FALSE FALSE = (λx.λy.x) FALSE FALSE = FALSE
XOR = NOT λx.λy.xy FALSE

Phew! Now this was quite a slog to get through! I am sincerely hoping I have not made any mistakes.