0
$\begingroup$

Use $\beta$ reductions to compute the final answer for the following $\lambda$ terms. Use a "fake" reduction step for "+" operator. Identify each redex for $\beta$-reduction steps. Does the order in which you apply these $\beta$-reduction steps make a difference in the final answer?

  1. (($\lambda$x.(($\lambda$z.(($\lambda$x.(z x)) 3)) ($\lambda$y.(+ x y)))) 1)

  2. (($\lambda$z. (($\lambda$y.z) (($\lambda$x.(x x))($\lambda$x.(x x))))) 5)

My solution for #1 was as follows:

(($\lambda$z.(($\lambda$x.(z x)) 3)) ($\lambda$y.(+ 1 y)))

(($\lambda$x.(($\lambda$y.(+ 1 y))x))3)

(($\lambda$x.(($\lambda$y.(+ 1 y)) x)) 3)

(($\lambda$y.(+ 1 y)) 3)

(+ 1 3)

4

However I couldn't get anything for #2, could someone please show me the process.

Also my interpretation is that the order does affect the answer, but I have no reasoning for it.

$\endgroup$
  • $\begingroup$ The Church-Rosser theorem says that if two sequences of reductions each reach a normal form, then it must be the same normal form; this is what justifies references to “the” normal form of a redex. $\endgroup$ – MJD Apr 18 '14 at 14:54
2
$\begingroup$

Your reduction of (1) is correct, except that you have $((λx.((λy.(+ 1 y))x))3)$ in there twice for some reason.

For 2, let's first abbreviate the subexpression $(λx.(x x))(λx.(x x))$ to $\omega$ as is often done. Then (2) is: $$((λz. ((λy.z) \omega)) 5)$$

$\omega$ is notorious because it is the simplest example of a $\lambda$-term with no normal form; it $\beta$-reduces in one step to $\omega$, and so an attempt to reduce it to normal form never terminates. However, we can still reduce the entire term as follows. First apply $(\lambda z. \ldots)$ to the argument 5, obtaining: $$((λy.5) \omega)$$

And again apply $(λy.5)$ to $\omega$ obtaining $$5$$

This is the normal form for the original expression. Since an attempt to reduce $\omega$ never terminates, the reduction order does make a difference. Notice that in obtaining the normal form, in each case we reduced the leftmost redex without first attempting to reduce its argument. This is called ‘normal-order’ reduction, and is guaranteed to produce the normal form of the expression, if it has one.

[ You didn't ask about this, but I found the redundant parentheses in your expressions extremely confusing, and I suggest that in the future you try to use fewer of them. ]

$\endgroup$

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.