[LINQ via C# series]

[Lambda Calculus via C# series]

Latest version: https://weblogs.asp.net/dixin/lambda-calculus-via-c-1-fundamentals

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

In lambda calculus, there are the conventions:

• Outermost parentheses are dropped: E₁ E₂ instead of (E₁ E₂)
• Applications are left associative: E₁ E₂ P may be written instead of ((E₁ E₂) P)
  • Again, E₁ E₂ P or ((E₁ E₂) P) will be E₁(E₂)(P) in C#
• The body of an abstraction extends as far right as possible: λx.E₁ E₂ means λx.(E₁ E₂) and not (λx.E₁) E₂
  • Here λx.E₁ E₂ will be x => E₁(E₂) 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#:

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.