Difference between $\beta$-contracts and $\beta$-reduces in Hindley

Question

I brought the book Lambda-Calculus and Combinators: An Introduction by J. Roger Hindley and the author explains what is $\beta$-reduction.

Now there is a difference between $\beta$-contracts and $\beta$-reduces: $$ \begin{align*} P &\rhd_{1\beta} P^\prime\\ P &\rhd_{\beta} P^\prime \end{align*} $$

Could someone please explain me what is the difference?

Answer 1

Notation and terminology varies a little between authors, so you should check the definitions used by the author. When you ask such questions, you should quote the definitions.

The expression “$P$ $\beta$-contracts to $P'$” means that $P$ contains a subterm which is an application and $P'$ is the result of substituting the argument into the abstraction body. That is, there exist $C$, $M$, $N$ and $x$ such that $P = C[(\lambda x.M) \, N]$ and $P' = C[[N/x] M]$ where $[N/x] M$ means the term obtained by substituting $N$ for $x$ in $M$ and $C[\cdot]$ is a term with a hole. Thus

• All terms of the form $(\lambda x.M) \, N \triangleright_{1,\beta} [N/x] M$ are $\beta$-contractions at the top of the term.
• If $P \triangleright_{1,\beta} P'$ then $M \, P \triangleright_{1,\beta} M \, P'$ and $P \, M \triangleright_{1,\beta} P' \, M$ and $\lambda x. P \triangleright_{1,\beta} \lambda x. P'$. The contraction is sometimes said to happen “in a context”.

The expression “$P$ $\beta$-reduces to $P'$” means that there is a chain of $\beta$-contractions that goes from $P$ to $P'$. For example:

• For any term, $P \triangleright_{\beta} P$ (a term reduces to itself in zero steps).
• If $P \triangleright_{1,\beta} P'$ then $P \triangleright_{\beta} P'$: a contraction is a reduction in one step.
• If $P \triangleright_{1,\beta} P'$ and $P \triangleright_{1,\beta} P'$ then $P' \triangleright_{\beta} P''$: a contraction in two steps.
• etc.

In a nutshell, a beta contraction is one step, a beta reduction is any number of steps. Note that some authors use different terminology and might call one step a beta reduction and many steps “a chain of beta reductions” or “a $\beta^*$ reduction”.