arrow_upward

MrMineev

λ Lambda Calculus

§

What is Lambda Calculus?

Lambda calculus is an abstract and elegant way of performing mathematics and solving problems using functions as its fundamental building blocks. It was developed by Alonzo Church in the 1930s. In lambda calculus, we work with special mathematical entities called "lambda functions." These functions take inputs and produce outputs based on rules defined within the functions. Think of them as magical boxes that you can put values into, and they will transform those values following specific instructions to give you a result. What makes lambda calculus unique is that everything is represented using these functions. There are no separate notions of objects, numbers, or booleans. Instead, numbers and other data types are encoded using clever combinations of functions. For example, instead of having a specific concept of a number, you can use functions to represent numbers. The number zero can be encoded as a function that takes two arguments and returns the first argument, while other numbers can be represented using different function compositions. Lambda calculus may seem very different from traditional math, but it has proven to be a powerful and foundational concept in computer science and mathematical logic. By working with functions and their combinations, lambda calculus allows us to express complex computations and solve various mathematical problems in a concise and universal way.

§

Notation

To define a function, you need to use the special lambda notation. Let's consider the simple function that has a function x as an input and returns the same function x. To write this function with Lambda notation, you have to write the following expression.

`lambdax. x`

To have a function have multiple arguments, you can write the following.

`lambdax. lambday. x`

This function takes two arguments and returns the first argument. Nice! Now how can we apply functions? Simple to apply a function x to an argument y; you can simply write the following.

`x" "y`

§

Encoding Booleans

As I said in the purest form of Lambda Calculus there is no such thing as numbers, booleans, etc. There are only functions. So to be able to work with booleans, we need to come up with an encoding for TRUE and FALSE. Let's encode TRUE and FALSE the following way.

`"TRUE" = lambdax. lambday. x`
`"FALSE" = lambdax. lambday. y`

How can we use this? Here is how we can define the NOT function using these definitions.

`"NOT" = lambdab. b " FALSE TRUE"`

For example, if you plug in TRUE into the NOT function, you will get the following.

`(lambdab. b " FALSE TRUE") " TRUE" rightarrow "TRUE FALSE TRUE" rightarrow "FALSE"`
`(lambdab. b " FALSE TRUE") " FALSE" rightarrow "FALSE FALSE TRUE" rightarrow "TRUE"`

You can also define AND, OR, and XOR using this notation the following way.

`AND = lambdaa. lambdab. a` `b` `a`
`OR = lambdaa. lambdab. a` `a` `b`
`XOR = lambdaa. lambdab. a` `(NOT` `b)` `b`

§

Encoding Numbers

Now that we know how to encode booleans, the next question is how to encode numbers. Simple!

`0 = lambdaf. lambdax. x`
`1 = lambdaf. lambdax. f x`
`2 = lambdaf. lambdax. f (f x)`
`3 = lambdaf. lambdax. f (f (f x))`
...

Using these encodings, you can define PLUS.

`PLUS = lambdam. lambdan. lambdaf. lambda x. m` `f` `(n` `f` `x)`

§

Recursion

Consider the factorial function.

`n! = {(1, n=0),(n * (n-1)!, n!=0):}`

Once you start thinking about this, you realize this isn't a trivial question. So let's break this down. We have a G-step function.

`G = lambdar. lambdan. (1, if n = 0; else` `n * (r` `(n - 1)))`

And then, we want some sort of FIX function that would do the following.

`F = FIX` `G`, where `FIX` `g = g * (FIX` `g)`

The fixed-point combinator FIX will return a self-replicating lambda expression representing the recursive function. Here is one of the possible definitions of FIX, the Y combinator.

`Y = lambdag. (lambdax. g` `(x` `x)) (lambdax. g` `(x` `x))`

§

Links


  https://en.wikipedia.org/wiki/Lambda_calculus


§

💬 Comments