skspot.blogg.se - Alpha reduction in lambda calculus

ALPHA REDUCTION IN LAMBDA CALCULUS FREE

Then in the body x + 1, x will be replaced by 2.First parameter name x and the => operator are ditched.For example, in C#, when applying this function x => x + 1 with argument 2:

ALPHA REDUCTION IN LAMBDA CALCULUS FREE

β-reduction / beta-reductionīeta-reduction of ((λV.E) R) is E, which means to substitute all free occurrences of the variable V in the expression E with expression R. Apparently it has nothing to do with the outer x. 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. This is also a perfectly nature normal thing, just like in C# function or lambda expression’s parameter can be renamed freely. This is called alpha-conversion, or alpha-renaming. In lambda calculus, lambda expression’s bound variables can be renamed. In lambda calculus, there are 3 ways that lambda expressions can be reduced. Lambda expression without free variables are called closed lambda expression, or combinator, which will be discussed later. Here alpha-conversion is used, which will be explained later. now clearly the single occurrence of xx is bound by the second lambda. This lambda expression must be rewritten as x => y(a => z(a)).

In C#, x => y(x => z(x)) does not compile, because the outer x variable conflicts with the inner x variable.

The single occurrence of x in the expression is bound by the second lambda.

All other variables are free variables.įor example, in the lambda expression from part 1 - λx.x + y or x => x + y, x is bound variable and y is free variable.Ī variable is bound by its "nearest" abstraction.

Variables within the scope of an abstraction are bound variables.

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

A sequence of abstractions is contracted: λx.λy.λz.E is abbreviated as λxyz.E.

Here λx.E 1 E 2 will be x => E 1(E 2) in C#.

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.

Again, E 1 E 2 P or ((E 1 E 2) P) will be E 1(E 2)(P) in C#.

Applications are left associative: E 1 E 2 P may be written instead of ((E 1 E 2) P).

Outermost parentheses are dropped: E 1 E 2 instead of (E 1 E 2).

In lambda calculus, there are the conventions:

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

If M, N ∈ Λ, then (E 1 E 2) ∈ Λ (called an application).

As fore-mentioned, λx.E is like x => E in C#.

If x is a variable and E ∈ Λ, then (λx.E) ∈ Λ (called a lambda abstraction, which defines a anonymous function).In lambda calculus, the set of lambda expressions Λ, can be defined recursively: Parentheses (), meaning higher precedence.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.The abstraction symbols lambda (λ) and dot (.).In lambda calculus, the syntax of lambda expressions are: This post will explain lambda expression and other concepts in lambda calculus. The C# lambda expression has been discussed in detail.