Will it be wrong to use g for reducing (λx.λy.x) first in step (2) instead of using to reduce λg?

Is there a rule against it?

enter image description here


You can do that, beta reduction can be applied at any point where an abstraction is immediately followed by application $((\lambda x. \cdots)t)$. In general, as you ovserved, there might be many redexes, i.e. many points where beta reduction can be applied.

However, note that sometimes we want to study what happens if we restrict ourselves to some reduction strategy. Essentially, a reduction strategy is a rule which chooses which redex to beta reduce when there are many. When doing that, there is a unique reduction sequence, a kind of unique execution run, for any term.

So, unless an exercise mandates the use of a specific reduction strategy, you are free to apply beta reduction at any point.

As a final remark, note that the choice of the redex can affect the termination of our reduction sequence. For instance, $(\lambda x.\ y)\Omega$ where $\Omega=(\lambda w.ww)(\lambda w.ww)$ can immediately reduce to $y$, or can loop indefinitely on reducing $\Omega$ to itself.

The Church-Rosser property (aka confluence, aka diamond property, mentioned above by xuq01) only ensures that, whenever we reduce a term $t$ with many beta reduction steps, possibly in two different ways leading to two terms $t_1,t_2$, there is a way to "reconcile" $t_1$ and $t_2$ and beta reduce those (in many steps) to a common form $t_f$.

This ensures that choosing the "wrong" beta redex does not compromise the reachability of the "intended" result (e.g. a normal form, if it exist). However, as seen in the example above, if we insist in selecting the "wrong" redex, it is possible that we get stuck into an infinite reduction sequence, when another one would lead to the intended result.

  • $\begingroup$ Alonzo Church is my personal superhero for the foundations of massively parallel computing! $\endgroup$ – Brian Haak Feb 4 at 21:51

No, you can try that and you'll get the same answer. Untyped lambda calculus has the Church-Rosser property, meaning that the order of $\beta$-reduction has no influence on the result of the reduction.

However, note that there is no guarantee that each term has a $\beta$ normal form, i.e. not necessarily exista a reduction sequence that leads to a final form. So, your term might diverge under one reduction order but not one other. However, if your term does have a $\beta$-normal form, the order of evaluation does not matter.


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.