# Lambda Calculus via C# (2) Fundamentals - Lambda Expression, Variables, Reductions

[Obsolete] See latest version - [Lambda Calculus]

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 (E
_{1}E_{2}) ∈ Λ (called an application)- The bigger difference is, while in lambda calculus, function application does not require parentheses () for parameter, it is just E
_{1}E_{2}; In C# it must be E_{1}(E_{2})

- The bigger difference is, while in lambda calculus, function application does not require parentheses () for parameter, it is just E

In lambda calculus, there are the conventions:

- Outermost parentheses are dropped: E
_{1}E_{2}instead of (E_{1}E_{2}) - Applications are left associative: E
_{1}E_{2}P may be written instead of ((E_{1}E_{2}) P)- Again, E
_{1}E_{2}P or ((E_{1}E_{2}) P) will be E_{1}(E_{2})(P) in C#

- Again, E
- The body of an abstraction extends as far right as possible: λx.E
_{1}E_{2}means λx.(E_{1}E_{2}) and not (λx.E_{1}) E_{2}- Here λx.E
_{1}E_{2}will be x => E_{1}(E_{2}) in C#

- Here λx.E
- 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:

- Variables within the scope of an abstraction are bound variables.
- All other variables are free variables.

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.