# Beta reduction in Lambda-Calculus

"A term of the form (λx.M)N, which consists of a lambda abstraction applied to another term, is called a β-redex. We say that it reduces to M[N/x], and we call the latter term the reduct. We reduce lambda terms by finding a subterm that is a redex, and then replacing that redex by its reduct."

Can someone tell me how to recognize a redex?

• It's a term of the form $(\lambda x.M)N$, just as it says in the first sentence, possible occurring somewhere inside a larger term (and recall that application is left-associative, so $z (\lambda x.x) y$ means $(z \lambda x.x) y$ and does not contain a redex). – Magdiragdag Feb 16 '18 at 9:48

Short answer: You can recognize a $\beta$-redex just as it says: it is any term where you have a left term applied to a right term, and the left term has the form $\lambda x.M$, where $x$ is a variable and $M$ is any term.

The idea is that terms of the form $\lambda x.M$ represent functions. By itself, the function does nothing and just sits there. But functions can be applied to arguments, and when that happens the application can be "reduced", or simplified.

You are already familiar with this. Consider the function that take some mathematical expression $x$ and adds it to itself. For example, it takes the expression $7$ and turns it into $7+7$, or it takes the expression $(a+b+1)$ and turns it into $(a+b+1)+(a+b+1)$. In lambda-calculus notation, this function is written $$\lambda x.x+x\tag{1}$$

By itself there is nothing we can do with this lambda term. But if we apply it to an argument, say like this: $$(\lambda x.x+x)(a+b+1)\tag{2}$$ now there is something to do: we can evaluate the function, which “reduces” the expression, yielding $x+x$, but with $x$ replaced by $(a+b+1)$, which is the term: $$(a+b+1)+(a+b+1).\tag{3}$$

Expression $(1)$ is not a reducible expression, but expression $(2)$ is a reducible expression. The phrase “reducible expression” is too long to say, so we just say redex. $(2)$ is a redex and $(1)$ is not. Expression $(3)$, the reduct of $(2)$, is also not a redex, unless we also know something about how $+$ works; whether it can be further reduced depends on the context of the discussion.

There could be several different kinds of reduction. For example, we might be using a version of lambda-calculus that has a rule that says that $7+7$ reduces to $14$. In that context, the expression $7+7$ would be a redex. In basic lambda calculus, $7+7$ is not a redex. To distinguish different kinds of reduction, we give them Greek letter names. The reduction you are concerned with here, the one which replaces the redex $$(\lambda x.M)N$$ with $$M[N/x],$$ is called $\beta$-reduction (for no good reason) and terms that can be $\beta$-reduced are called $\beta$-redexes.

$\beta$-redexes are easy to recognize, and the paragraph you quoted tells you exactly what they look like. There must be a left term applied to a right term, and the left term must have the form $\lambda x.M$ for some variable $x$ and some term $M$. That is, there must be a function, and it must be applied to some argument. Then you reduce it by substituting the argument into the body of the function in place of the function's parameter, just as you apply $\sin(x)$ to the argument $2\pi$ to get $\sin(2\pi)$, or $\sqrt {y+2}$ to the argument $17$ to get $\sqrt{17+2}$.

Is $7+7$ a redex? Maybe, it depends on the context. But is it a $\beta$-redex? No, it is not, because it is not an application of a left term to a right term.

(Reductions like $7+7\to 14$ are sometimes called $\delta$-reductions; there is also an $\eta$-reduction you may see later, and an $\alpha$-reduction which is often called “$\alpha$-conversion” instead because it does not actually reduce anything.)