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?


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”.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.