# How to find a function in Lambda Calculus?

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

• 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! – Raphael Sep 16 '18 at 10:59

$$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.

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