0
$\begingroup$

Yesterday I have been trying to complete this exercise. I have to find: $$ ((map)l)t \simeq \lambda k \lambda x ((k)(t)t_1)....((k)(t)t_n)x $$

where $$l=\lambda k \lambda x ((k)t_1)....((k)t_n)x$$ And $t$ is a generic Lambda term. I tried but without success. Maybe it will be something like that : $$map=(\lambda a \lambda b (\lambda s \lambda d((b(st))d)))$$ Thank you in advance to all will answer

$\endgroup$
  • 1
    $\begingroup$ Welcome to Computer Science! The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$ – Raphael Sep 16 '18 at 10:59
1
$\begingroup$

In your attempt,

$$map=(\lambda a \lambda b (\lambda s \lambda d((b(st))d)))$$

$a$ plays the role of $l$, $b$ the role of $t$, $s$ the role of $k$, and $d$ the role of $x$.

So, $b(st)d$ should actually play the role of $l(kt)x$, but here we see some mismatch: $b$ does not represent $l$, $a$ does that. Also, we can not use $t$, but must use $b$ instead.

Hence, the correct answer seems to be $a(sb)d$. We get (using the standard notational shortcuts)

$$map=(\lambda a b s d.\, a(sb)d)$$

Try to check whether $map\, l\, t$ does $\beta$ convert to the intended term.

Your original idea, namely using $kt$ instead of $k$, seems to be the right intuition, as far as I can see.

$\endgroup$
  • $\begingroup$ I think that I had done a mistake when I wrote my version of $$map$$ here. Now it's clear. Thank you so much! $\endgroup$ – Alessandro Recchia Sep 16 '18 at 13:52

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.