Lambda Abstraction

lambda-calculus

Definition

Lambda Abstraction

The syntactic construct $\lambda x.e$ is called a lambda abstraction, where $x$ is a bound variable and $e$ is an expression.

todo

Halting

Lambda expression do not necessarily halt. Example:

$$(\lambda x.xx)(\lambda x.xx){\to }_{\beta }(\lambda x.xx)(\lambda x.xx){\to }_{\beta }\dots$$

Thus, the Halting problem applies here.

Beta Equivalence

Definition

Beta Equivalence (Lambda Calculus)

Two lambda abstractions $M,M^{\prime }$ are beta-equivalent, $M{=}_{\beta }{M}^{\prime }$ if $M$ can be transformed into $M^{\prime }$ by $n\ge 0$, possibly inverse, beta reductions.

Link to original