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

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:

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#:

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

It can be reduced to:

1
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.