Multiple inputs in lambda calculus (Confusing example)

Question

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

Answer 1

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

Answer 2

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

Let's follow each step:

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.