---
title: Lambda calculus 1
date: 26 July 2022
---

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:

a) `x - y + 2z`, then `λx.λy.λz.x - y + 2z`
b) `-x + 5`, then `λx.- x + 5`
c) `a^2+b^2-c^2`, then `λa.λb.λc.a^2 + b^2 + c^2`
d) `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.