Is it not grand enough to have the same computational power as Turing machines? Then, Lambda Calculus can achieve the creation from nothingness to duality, from duality to the four phenomena, and from the four phenomena to the eight trigrams. Thanks to Church, we finally obtained everything in the world.

Lambda Calculus, also known as λ-calculus, is a formal system used to study function definition, implementation, recursion, and is the computational model for functional languages.

Definition

A λ-expression should consist of the following parts:

  • Variables: v1, v2, . . .
  • Symbols: λ and .
  • Parenthesis pairs: ( and )

A valid λ-expression can be recursively defined as follows:

  • <expression> = <variable> | <function> | <application>
  • <function> = λ <variable>.<expression>
  • <application> = (<expression> <expression>)

λ-Expression Notation

For λ-expressions M and N,

  • The outermost parentheses can be omitted, so (M N) can be represented as M N.
  • (λx. M) is called function abstraction, as it often represents a function definition. The function parameter is variable x, the function body is M, and the function name is anonymous. You can think of it as f(x)=M, where the function name f is non-existent, and only the mapping process from x to M exists.
  • Function application is left-associative: M N P means (M N) P.
  • λ-expressions use greedy expansion: meaning λ x. M N represents (λ x.M N) rather than (λ x. M) N.
  • λ-expression sequence: λ x λ y λ z. N can be abbreviated as λ x y z . N.

Free Variables and Bound Variables in λ-Expressions

The function abstraction operator λ can bind any variables that appear in the body of the function abstraction. If a variable is within the scope of a λ-expression, then the variable is considered bound. Otherwise, the variable is free.

For example, in the expression λ y . x x y, y is a variable bound by λ, while x is a free variable.

A λ-expression M consisting of a series of free variables can be represented as FV(M) and is recursively defined as follows:

  • FV(x) = {x}, where x is a free variable
  • FV(λ x . M) = FV(M) - {x}
  • FV(M N) = FV(M) ∪ FV(N)

A λ-expression that does not contain free variables is called closed.

Reduction Methods

α-conversion

It's just symbol replacement. It's not very interesting, except that it allows for renaming of symbols during reduction if symbol name conflicts occur. However, α-conversion is only valid in the current domain. For the expression λ x x. x, it can be converted to λy x. x, but not to λy x.y. Because names themselves are unimportant in λ-expressions.

Replacement: E[V:=E'] denotes that variable V can be replaced with E', if E' is free in E.

For example, (λx. y)[y:=x] resulting in (λx. x) is incorrect because x is bound under λ. The correct method is through α-conversion to (λz. y)[y:=x] resulting in (λz.x).

β-reduction

This represents the idea of function application.

For the expression (M N), the meaning is to apply function M to N. That is, N is passed as an argument into function M, serving as a bound variable within M. Using the definitions above, β-reduction (λ v. m) n can be represented as m[v:=n].

For instance, if there is a function λ x. (+ x 2) and the + operation is defined, then (λ x. (+ x 2)) 3 results in (+ 3 2) = 5.

η-conversion

This expresses the idea of "extensionality."

If two functions are equivalent, then they must yield consistent results for all input parameters. That is, for these two functions, performing β-reduction or α-conversion should yield identical λ-expressions.

From Zero to Everything

Now, we can start playing with λ-calculus. Remember, aside from what we've discussed, we have nothing, not even the concept of 'number'.
So, the first thing is the [definition