# Multiple inputs in lambda calculus (Confusing example)

In a programming class I take, we briefly (very briefly) touched lambda calculus. I think I have a pretty good grasp of the basics now, but one example given I just don't understand. Am I missing something or is the example possibly false?

$$\lambda x.x \; (\lambda y.2*y) \; square \; 3$$

The solution to this was $$6$$, because $$\lambda x.x$$ (the first function) is applied to $$square$$ (the first input) which just "disappears" and $$\lambda y.2*y$$ is applied to $$3$$, which gives us $$6$$:

$$\lambda x.x \ (\lambda y.2*y) \ square \ 3 \implies (\lambda y.2*y) \ 3 \implies 2 * 3 \implies 6$$

EDIT

Regardless of whether the "disappearance" of $$square$$ is correct, why would the first step be to apply $$\lambda x.x$$ to $$square$$ ? Instead of the whole expression, or just the part in parenthesis (which would, afaict, give the same result). I.e., what way of parenthesising is implied from the way it's written above?

/EDIT

The way I understand it, it should be either 18, because:

$$\lambda x.x \; (\lambda y.2*y) \; square \; 3$$ with parenthesis should be:

$$(((\lambda x.x \; (\lambda y.2*y)) \; square) \; 3)$$ which gives me:

$$(((\lambda y.2*y) \; square) \; 3) \implies ((2*square) \; 3) \implies 2 * square(3) \implies 2 * 9 \implies 18$$

or nothing at all, i.e. $$((2*square) \; 3)$$ doesn't make sense.

Another example that was given:

$$(\lambda f.(\lambda x.f(f \; x))) \; square \; 3 \implies (\lambda x.square(square \;x)) \;3 \implies square(square \; 3) \implies square(9) \implies 81$$

This second example seems clear to me, I'm just adding it to show something similar.

How would one properly solve $$\lambda x.x \; (\lambda y.2*y) \; square \; 3$$ ?

• Welcome to Computer Science! It would be nice if you can provide a reference in the question to the example thereof so that people can have more context to understand and answer your question more effectively. Nov 23, 2018 at 1:26
• Thanks. I updated the question to hopefully clear up what I mean.
– user96726
Nov 23, 2018 at 7:34

The problem is in (most likely wrongly) parenthesising expressions.

$$\lambda$$ abstraction goes as far right as it can, so your whole example is just one abstraction with body $$x\ (\lambda y. 2 \cdot y)\ \texttt{square}\ 3$$, meaning that there is nothing to be applied to $$\lambda x$$, thus no "level-0" redexes. There is just one redex in here, namely $$\require{enclose} \enclose{horizontalstrike}{(\lambda y. 2\cdot y)\ \texttt{square}}$$, reducing to $$\require{enclose} \enclose{horizontalstrike}{(2\cdot \texttt{square})}$$. There is also no redexes within the body because if we fully parenthesise the original expression (having in mind that $$\lambda$$ applications (within the body) are left associative) we get $$\lambda x. \biggl(\Bigl(\bigl(x\ (\lambda y. 2 \cdot y)\bigr)\ \texttt{square}\Bigr)\ 3\biggr)$$

If we want to make it reduce to $$6$$, we must completely ignore $$\texttt{square}$$, because no natural number squared gives $$6$$. We can do that by making it an input to abstraction that doesn’t use it. $$\bigl(\lambda x.(\lambda y.\ 2 \cdot y)\bigr)\ \texttt{square}\ 3$$

• That's what I thought. To clarify then, what would the implied way of parenthesising? $\lambda x.(x((\lambda y.2 \cdot y) \ square) \ 3)$ ? And can $\lambda x.x \ (2 \cdot square) \ 3$ be reduced any further?
– user96726
Nov 23, 2018 at 7:51
• Thanks for the comment. I realized I made a mistake and updated my answer, and also answered your question about fully parenthesising. Nov 23, 2018 at 8:56
• It can't be reduced any further as is. If we provided definitions for $\cdot$ and $\texttt{square}$, we would likely be able to reduce portions of it, but the overall form would stay the same - $x\ (\lambda y. *) * 3$, where '*' represents 'something' Nov 23, 2018 at 9:16

In $$\lambda$$-calculus, every abstraction (= function) is unary.

For this reason, $$square$$ is the argument replacing $$x$$ and once it only remains the body of the function, 3 can be supplied as argument, replacing $$y$$.

1. $$\lambda x.x (\lambda y.2 * y) \ square \ 3$$

2. $$\beta$$-reducing the first redex $$\lambda x.x (\lambda y.2 * y) \ square$$ gives the following result:

$$square (\lambda y.2 * y) \ 3$$

From here on, we would need the $$\lambda$$-definition of $$square$$, but I would imagine it would only accept a single argument, the base.

The problem is that the argument 3 would then be passed to the result of this redex $$square (\lambda y.2 * y)$$, differently from the hint that 3 would be passed to $$(\lambda y.2 * y)$$ and afterwards the $$square$$ would be executed.

If instead, the $$\lambda$$-term would have been defined in the following ways, it would have had much more sense; I still cannot understand how $$square$$ can completely disappear from the computation.

1. $$\lambda xy.x (2 * y) \ square \ 3 \implies square(2*3) \implies 36$$

2. $$\lambda xy.2 * x y \ square \ 3 \implies 2*square(3) \implies 2 * 9 \implies 18$$

3. $$\lambda xyz.x(yz) \ square \ (\lambda y.2 * y) \ 3 \implies square((\lambda y.2 * y) \ 3) \implies square(2*3) \implies square(6) \implies 36$$

The second example is perfectly fine to me.

• Thank you for the explanation, that clears it up a bit. I guess my question would be more precisely, why is the first redex $\lambda x.x (\lambda y.2 * y) \ square$ instead of just $\lambda x.x (\lambda y.2 * y)$ ? And yes, the second example was clear to me as well, I just added it to show a similar example.
– user96726
Nov 22, 2018 at 16:44
• I actually didn't think about $\lambda x.x$ as the first abstraction, assuming the complete body was $x(\lambda y.2 * y)$. If instead we consider the following $\lambda$-term: $(\lambda x.x) \ (\lambda y.2 * y) \ square \ 3$, then of course the computation proceeds with the following steps: $(\lambda y.2 * y) \ square \ 3 \implies 2 * square \ 3$, which again would depend on the definition of $square$. There still is the problem that $2 * square$ should be processed first and then $3$ passed in as argument, which isn't correct. Some parentheses may be missing, probably in the last arg Nov 22, 2018 at 21:15