What is beta reduction in lambda calculus?

Beta reduction, essentially a substitution, is a process in lambda calculus for reducing lambda expressions.

Note: Lambda calculus is a computation model that works with lambda expressions. It lays down the foundation of every functional programming language.

Understanding the notation for a lambda expression

The following is a sample lambda expression:

$(\lambda x.xy )z$

Every lambda expression is interpreted as the following:

$(\lambda\ parameter\ .\ output)\ input$

Beta reduction works by finding all the occurrences of the parameter ($x$) in the output ($xy$) and substituting the input ($z$) for that parameter ($x$) in the output ($xy$) that gives us the reduced result ($zy$).

Structure of a lambda function

A lambda function ($\lambda$) takes a function as input and outputs a new function. Intuitively, it can be interpreted as the following equation:

$f(x) = \{xy\ |\ x=z \}$

Here, $f$ is the function name, $x$ is the function parameter, and $xy$ is the expression to be solved by substituting the value of $x$ that is $z$.

In a programming language, it can be mapped to the following function:

The notation for lambda expression doesn’t require function names. It represents the function with lambda ($\lambda$).

Notation and rules for beta reduction

• Parameters $\lambda mno$ can also be written as $\lambda m.\lambda n. \lambda o$.
• The substitution expression for $(\lambda m.m)(\lambda x.xx)$ is written as $(m)(m:= \lambda x.xx)$. We remove the parameter $\lambda m$ and write the substitution for $m$ in notation $(m:= \lambda x.xx)$.
• $(m)(m:=λx.xx)$ is evaluated as $λx.xx$. We substituted the value of $m$ in place of all the occurrences of $m$ in the output (a single occurrence of $m$ in the output in this case).

Alpha conversion is just about changing the names of the same name variables while applying multiple lambda expressions with the same variable name. For example, $(λy.y)(λyz.y)$ changes to ($λy.yy)(λy_{1}z.y_1)$. We perform this step before beta reduction if the lambda expressions have the same name and cause name conflict.