Using beta reduction on $ \lambda y. ( \lambda x. \lambda y. y x)(\lambda z. y z)$

98 Views Asked by At

I have a few questions regarding this exercise:

$$ \lambda y. ( \lambda x. \lambda y. y x)(\lambda z. y z)$$

This is what I have come up with:

$ \lambda y. ( \lambda x. \lambda \color{red}u. \color{red}u x)(\lambda z. y z) = \lambda y. ( \lambda u. u (\lambda z. y z))$

My questions are:

1. While analyzing the expression from left to right, I have two lambda expressions: $\lambda y.$ and $ (\lambda x. \lambda y. yx)$ I would need to apply the first one to the second one (i.e. "plug in" the 2nd one in the 1st one) which doesn't make sense. This is why I opted to apply $ (\lambda x. \lambda y. yx)$ to $(\lambda z. y z)$

2. By applying $ (\lambda x. \lambda y. yx)$ to $(\lambda z. y z)$, I changed the name of the variable "y" to "u" in the first expression since it is bound there, and it also appears in the second expression. Did I perform a correct alpha-conversion? Can I reduce this further?

3. I am always confused then I have something like this: $u(\lambda z. yz)$. I would know what to do if I had $(\lambda z. yz)u$: I'd apply the function to the argument $u$. However, now that their positions are reversed, I don't know what to do.

Any help would be greatly appreciated!

1

There are 1 best solutions below

3
On

Remember that a $\lambda$-term is either (a) a variable $x$, (b) an abstraction $(\lambda x.t)$, where $x$ is a variable and $t$ is a $\lambda$-term, or (c) an application $(st)$, where $s$ and $t$ are $\lambda$-terms.

The issue with your example is that it is ambiguous: it could be read as an abstraction $$\lambda y. [( \lambda x. \lambda y. y x)(\lambda z. y z)]$$ or as an application $$[\lambda y. ( \lambda x. \lambda y. y x)](\lambda z. y z)$$

I suspect that the first reading is what is intended. Note that for the grammar I gave above, where abstractions and applications are always wrapped in parentheses, we would formally write this as $$(\lambda y.((\lambda x.(\lambda y.(yx)))(\lambda z.(yz)))).$$ It's annoying to write so many parentheses, so people usually leave them out when there's no chance for ambiguity. But you have to be careful about this. You may have some conventions in play so that this expression can be parsed unambiguously. But in any case, I would prefer to use extra brackets in this case for clarity.

For the first reading $\lambda y. [( \lambda x. \lambda y. y x)(\lambda z. y z)]$, sparusaurata has already answered questions 2 and 3 in the comments: Your $\alpha$-conversion and $\beta$-reduction are correct, and there is no more reduction you can do at this stage. Intuitively, $u$ is a variable standing for a "function", but until you know what "function" it is, you can't apply it to its input $(\lambda z. yz)$.

For the second reading $[\lambda y. ( \lambda x. \lambda y. y x)](\lambda z. y z)$, you $\beta$-reduce by substituting $(\lambda z.yz)$ for all free occurrences of $y$ in $(\lambda x. \lambda y. y x)$. But there are no free occurrences of $y$ in this $\lambda$-term, so after $\beta$-reducing, we just get $(\lambda x. \lambda y. y x)$.