1
$\begingroup$

I have the following and am asked to evaluate it (I've posted this question elsewhere but I have a new worry with evaluating the function).

$[[\lambda f.\lambda m. f(m + m^2))]([\lambda n.2n])](3)$

I'm worried about mis-evaluating this because I'm putting brackets in the wrong place.

Here's my reasoning thus far.

  1. I bind $\lambda n.2n$ to $f$ to get the following:

$[[\lambda m.[\lambda n.2n](m+m^2)](3).$

  1. Then I bind $(m+m^2)$ to $n$ to get the following:

$[\lambda m.2(m+m^2)](3)$

  1. And then finally I bound (3) to $m$ to get this:
    $2(3+3^2)$ which equals 36.

I'm worried that at (2) I should bind THREE to $m$ and gotten this instead:
$\lambda n.2n(3+3^2)$ and THIS should be my end result.

Does anyone have any thoughts, tips, suggestions or see any mistakes or anything? Help would be greatly appreciated; I'm really struggling with Lambda Calculus stuff.

$\endgroup$
1
$\begingroup$

Sorry for such a late response. I hope it at last helps others if you already figured everything out.

There is a Church-Rosser theorem which deals with your concern exactly. It states that the order of reductions is irrelevant and if we apply, say, $2$ different reductions to the expression yielding $2$ different resulting expressions, then there must be an expression that is reachable from both of them. In your example, $24$ will be reachable no matter what we decide on step $2$.

Let us now discuss your steps. Almost all of your reductions are done correctly (except the one you worry about), and I am quite sure that $2(3+3^2)$ is $24$ and not $36$ :).

You say that you worry about substituting $3$ for $m$ in the expression $[\lambda m.[\lambda n.2n](m+m^2)]$, but you then make a mistake in doing so (you forget brackets around $\lambda n.2n$). The result should be \begin{equation} [\lambda n.2n](3+3^2) \end{equation} which is then also $24$.

Leaving out those brackets changed the semantics of your expression because by definition $\lambda$ goes as far as possible, so by removing those brackets you were left with just the $\lambda$-abstraction $\lambda n. 2n(3+3^2)$ but it was supposed (all along through task) to be the application of $\lambda n. 2n$ onto $(3+3^2)$.

$\endgroup$
  • $\begingroup$ For the untyped lambda calculus, I believe you only have that every path leaves the normal form reachable (if it exists), not that every path reaches it. $\endgroup$ – Mjiig Aug 20 '18 at 13:48
  • $\begingroup$ You are right. I will correct my response $\endgroup$ – Sandro Lovnički Aug 20 '18 at 13:53

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.