Lambda Calculus via C# (2) Fundamentals - Lambda Expression, Variables, Reductions
[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.
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:
- 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.
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:
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.