 # [Lambda Calculus via C# series]

The C# lambda expression has been discussed in detail. This post will explain lambda expression and other concepts in lambda calculus.

# Lambda expression

In lambda calculus, the syntax of lambda expressions are:

• Variables v1, v2, …, vN
• The abstraction symbols lambda (λ) and dot (.)
• For example, the C# lambda expression x => x + 1 will be λx.x + 1 in lambda calculus, except the C# specific type system (Int32, Int 64, …) does not exist in λx.x + 1.
• Parentheses (), meaning higher precedence

In lambda calculus, the set of lambda expressions Λ, can be defined recursively:

• If x is a variable, then x ∈ Λ
• If x is a variable and E ∈ Λ, then (λx.E) ∈ Λ (called a lambda abstraction, which defines a anonymous function)
• As fore-mentioned, λx.E is like x => E in C#
• If M, N ∈ Λ, then (E1 E2) ∈ Λ (called an application)
• The bigger difference is, while in lambda calculus, function application does not require parentheses () for parameter, it is just E1 E2; In C# it must be E1(E2)

In lambda calculus, there are the conventions:

• Outermost parentheses are dropped: E1 E2 instead of (E1 E2)
• Applications are left associative: E1 E2 P may be written instead of ((E1 E2) P)
• Again, E1 E2 P or ((E1 E2) P) will be E1(E2)(P) in C#
• The body of an abstraction extends as far right as possible: λx.E1 E2 means λx.(E1 E2) and not (λx.E1) E2
• Here λx.E1 E2 will be x => E1(E2) in  C#
• A sequence of abstractions is contracted: λx.λy.λz.E is abbreviated as λxyz.E
• λx.λy.λz.E is x => y => z => E in C#
• λxyz.E is (x, y, z) => E in C#

# Bound and free variables

In lambda expression, λ or => means to bind its variable wherever it occurs in the body. So:

For example, in the lambda expression from part 1 - λx.x + y or x => x + y, x is bound variable and y is free variable.

A variable is bound by its "nearest" abstraction. For example, in λx.y (λx.z x):

• The single occurrence of x in the expression is bound by the second lambda.
• In C#, x => y(x => z(x)) does not compile, because the outer x variable conflicts with the inner x variable. This lambda expression must be rewritten as x => y(a => z(a)). now clearly the single occurrence of xx is bound by the second lambda. Here alpha-conversion is used, which will be explained later.

Lambda expression without free variables are called closed lambda expression, or combinator, which will be discussed later.

# Reductions

In lambda calculus, there are 3 ways that lambda expressions can be reduced.

## α-conversion / alpha-conversion

In lambda calculus, lambda expression’s bound variables can be renamed. This is called alpha-conversion, or alpha-renaming. This is also a perfectly nature normal thing, just like in C# function or lambda expression’s parameter can be renamed freely.

In the above example of λx.y (λx.z x), the inner lambda expression λx.z x can be alpha-converted to λa.z a. Apparently it has nothing to do with the outer x.

## β-reduction / beta-reduction

Beta-reduction of ((λV.E) R)  is E[V := R], which means to substitute all free occurrences of the variable V in the expression E with expression R. It is just function application. For example, in C#, when applying this function x => x + 1 with argument 2:

• First parameter name x and the  => operator are ditched.
• Then in the body x + 1, x will be replaced by 2. So the result of function application is 2 + 1.

## η-conversion / eta-conversion

Eta-conversion means 2 functions are the same if and only if they give the same result for all arguments. It converts between λx.(f x) and f whenever x does not appear free in f. Here is an example in C#:

```Func<int, bool> isEven = x => x % 2 == 0;
Enumerable.Range(0, 5).Where(x => isEven(x)).ForEach(x => Console.WriteLine(x));```

It can be reduced to:

`Enumerable.Range(0, 5).Where(isEven).ForEach(Console.WriteLine);`

Here x => isEven(x) and isEven are the same, and x => Console.WriteLine(x) and Console.WriteLine are the same too (C# compiler will pickup the right overload - Console.WriteLine(int value)).

Different reduction order can be applied to the same lambda expression and have different impact. This will be demonstrated in a later part. 