1
$\begingroup$

given the input

(((lambda f (lambda x (f x))) (lambda y (* y y))) 12)

what does this step evaluate to: lambda x (f x)

I am trying to evaluate this and I have the following tree so far:

enter image description here

how do I evaluate this ? looking for guidance on what I might be doing wrong or how to proceed with this.

$\endgroup$
2
  • $\begingroup$ The tree is inconsistent. There are no "apply" nodes under "lambda" nodes. However, f is applied on x and (*) is applied on y and the result is again applied on y. $\endgroup$
    – frabala
    Mar 23 '20 at 19:41
  • $\begingroup$ The tree written is correct. Apply is just implicit in lambda calculus, indicated by concatenation. $\endgroup$
    – DanielV
    Mar 24 '20 at 0:16
1
$\begingroup$

Lambda expressions are evaluated by reducing the leftmost redex first. A redex is something of the form $(\lambda a.b)c$ . Your expression is $(\lambda f.\lambda x.fx)(\lambda y . *yy)~12$. So your first redex is

$$(\lambda f.\lambda x.fx)(\lambda y . *yy)$$

So you substitute $(\lambda y . *yy)$ for $y$ in $\lambda x.fx$ to get $$\lambda x.(\lambda y . *yy)x~ 12$$

Then your next redex is the entire expression, ($(\lambda y . *yy)x$ is also a redex but it isn't the leftmost one) substituting $12$ in for $x$. So you get $$(\lambda y . *yy)~12$$

Then your last redex is the entire expression again so you get

$$*~12~12$$

$\endgroup$
3
  • $\begingroup$ the leftmost redex concept is a little hard for me. What if the redex thats we are substituting is more complex that the one in this case, can we simplify it before substituting ? For E.g. (lambda y (lambda g (g (* y y)))) $\endgroup$
    – Dhruv
    Mar 24 '20 at 4:14
  • 1
    $\begingroup$ @Dhruv The expression you wrote there isn't a redex, I'll assume you mean it as the $c$ for some $(\lambda a.b)c$ . And the answer is...sometimes. Evaluating left to right gives you the property that if the lambda expression has a redex-free final form, then you will reach it. If you evaluate in arbitrary order, you could loop forever. $\endgroup$
    – DanielV
    Mar 24 '20 at 6:45
  • $\begingroup$ I posted another question to cs.stackexchange.com/questions/122115/… as a follow up. $\endgroup$
    – Dhruv
    Mar 25 '20 at 2:39

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.