User:I am islptng/Lambda Calculus Tutorial

From Esolang
Jump to navigation Jump to search
Thanks for YouTuber 2swap (His video helps a lot.)

Since I was confused about lambda calculus at first, and I took a long time to understand it. So I'll write this article to help others.

Also evaluating lambda expressions is a good way to kill my time. :D

What is Lambda calculus?

It's a computation model that is Turing Complete. (I just can't believe this at first; I'll explain the key part that make me finally convinced later)

In this world, everything is a lambda function. Computing is just a function applied to another.

Syntax

Every lambda calculus program follows the 3 templates:

  1. Variable: a or anything you can use for a variable.
  2. Applying: (fx) which applies f to x.
  3. Lambda: λx.y which means a lambda with an argument x and it evaluates to y.

Currying

Let's say, λxy.z is equivalent to λx.λy.z, and abc is equivalent to ((ab)c).

This simplifies the notation.

Computation steps

You have 3 things to do with lambda expressions:

α-conversion

This allows you to rename variables. For example,

λfgx.fx(gx)

is equivalent to

λabc.ac(bc)

β-reduction

This is the key process of computation. There's no much difference between this and function calling if you know how to code in modern languages.

For example, λfgx.fx(gx) ABC actually is the same as this Python code:

(lambda f:(lambda g:(lambda x:f(x)(g(x)))))(A)(B)(C)

And of course, it becomes AC(BC).

The conversion from λfgx.fx(gx) ABC to AC(BC) is called β-reduction.

η-conversion

This allows you to say, λx.x A is equivalent to A, since the former β-reduces to the latter.

Church numerals and booleans

We define,

False = λxy.y
True = λxy.x

And numbers?

0 = λfx.x
1 = λfx.(fx)
2 = λfx.(f(fx))
3 = λfx.(f(f(fx)))
...

Examples

Combinator calculus

Wait for me to understand it completely.