# How to define $f(x) = 2x$ as a recursive and lamba function?

How can I exhibit a recursive function and a $\lambda$-term simulating the function $f : \mathbb{N} \rightarrow \mathbb{N}$, such that $f(x) = 2x$?

For $\lambda$ part, I thought to create a mult function defined like mult = $\lambda nmf.n(mf)$. And of course, Church numberal are defined in the following manner, $\overline{n} = \lambda fx.f^nx$ (eg. $\overline{3} = \lambda fx.f(f(f(x)))$. I tried to test my mult function with simple parameters, but I kind of got stuck, I assume there is some simplification in order to reach the final result of $\overline{4}$ in my example.

$$\text{mult} \space \overline{2} \space \overline{2} = \lambda nmf.n(mf) \space (\lambda fx. f(fx)) \space (\lambda fx. f(fx)) \\ \rightarrow \beta \qquad \lambda nf.n((\lambda fx. f(fx))f) \space (\lambda fx. f(fx)) \\ \rightarrow \beta \qquad \lambda f.(\lambda fx. f(fx)) \space ((\lambda fx. f(fx))f) \\ = \lambda f. f((\lambda fx. f(fx))f)$$

But, then how can I finish this in order to get $\overline{4}$, and how can I transform my mult function, to the function in the problem $f(x) = 2x$. Can I transform my mult to a partial function application, where I apply to it $\overline{2}$ as the first parameter, and then use it as my $f(x) = 2x$? I mean mult2 = $\lambda nf. n(\lambda fx. f(fx)f) = f(x) = 2x$.

On the other hand, for the recursive function part. I have the following functions. Therefore, I tried to do something like below, but I don't know whether it is correct.

$$f(0) = \text{zero}^1(x) \\ f(x+1) = h(x, \text{prod}(2,x), 2) \qquad \text{where h is defined as} \\ h(u,v,w) = \text{prod}(\text{proj}_2^3(u,v,w), \text{proj}_3^3(u,v,w)) \quad \text{so, we get} \\ f(x+1) = h(x, \text{prod}(2,x), 2) = \text{prod}(\text{prod}(2,x),2) = 2 \cdot x \cdot 2$$

Any ideas whether they are correct, and if not how to fix them?

I think you have to change your $h$ function: $f(x+1) = 4x$ is wrong!

Set $h(u,v,w) = \text{sum}(\text{proj}^3_2(u,v,w), \text{proj}^3_3(u,v,w))$ and then you get $f(x+1)=h(x,\text{prod}(2,x),2) = \text{sum}(\text{prod}(2,x),2) = 2x + 2$.

As for the $\lambda$-term, I don't understand the last passage in your example. In my opinion: \begin{align*} \text{mult} \, \overline{2} \, \overline{2} &\to_\beta^* \lambda f.(\lambda fx.f(fx)) ((\lambda fx.f(fx))f) \\ &\to_\beta \lambda f.(\lambda fx.f(fx)) (\lambda x.f(fx)) \\ &\to_\beta \lambda f x. (\lambda x.f(fx)) ((\lambda x.f(fx))x) \\ &\to_\beta \lambda fx.(\lambda x.f(fx)) (f(fx)) \\ &\to_\beta \lambda f x. f(f(f(fx))) = \overline{4} \end{align*}

More generally, I think that your answer concerning the $\lambda$-calculus is correct. You can "optimize" your answer, i.e. reduce the number of $\beta$-steps that are necessary to compute the output. Indeed: \begin{align*} \text{mult} \, \overline{2} &= (\lambda n m f. n(mf)) (\lambda fx. f(fx)) \\ &\to_\beta \lambda mf. (\lambda fx. f(fx))(mf) \\ &\to_\beta \lambda mfx.(mf) ((mf)x) \end{align*} hence you can take $\lambda mfx.(mf) ((mf)x)$ as $\lambda$-term representing the function $f \colon \mathbb{N} \to \mathbb{N}$ such that $f(x) = 2x$.

• Yes, thanks, I fixed the typo. And yes, seems like just replacing the first $\text{prod}$ with $\text{sum}$ works just fine. Any idea for the lambda part, thought? – user72151 Jan 3 '16 at 14:18
• @Yuko: I edited my answer, now there is a part about $\lambda$-calculus. I hope it is clear! – Taroccoesbrocco Jan 3 '16 at 17:03
• Yes, it is clear to certain extend, thanks. I have just one remark that are not clear to me. In your $\text{mult} \, \overline{2} \, \overline{2}$ reductions, when you go from second reduction to third one, you have again introduced $x$. Because it was $\to_\beta \lambda f.$, and then it is $\to_\beta \lambda f x.$, and there is an $x$ at the end. Is it legal to do these kind of operations in lambda calculus when we apply reductions? Cause you have done the same thin in the last step of $\text{mult} \, \overline{2}$ reduction. Otherwise, it is fine, I can follow and understand it all. – user72151 Jan 3 '16 at 21:27
• @Yuko: in general, by definition, $\lambda f.\lambda x. t = \lambda fx.t$: they are the same $\lambda$-term. – Taroccoesbrocco Jan 3 '16 at 21:46

$$M=\lambda nmfx.n(mf)x \Leftrightarrow M=\lambda nmf.n(mf)$$

Hence $$M(\lambda fx.f^nx)(\lambda fx.f^mx)fx=(\lambda fx.f^nx)(\lambda x.f^mx)x=f^{mn}x$$

For the second part $2(x+1)=2x+2$, just compose $succ$ with itself for $h$, you don't need a product !