I can't have a confidence of my this lambda calculus of $~\left(\lambda x ~.~ (x~z) \right)~$

Question

I want to evaluate the below lambda term correctly.

$$ \color{blue}{\left(\lambda x ~.~ (x~z) \right)} $$

Here I assume $~ x,z ~$ are mutually independent.

Namely not a kind of $~ x(t),z(t) ~$or $~ z=\sin(x)~\text{and}~x~\text{is independent} ~$

$$\begin{align} g:&=\left(\lambda x ~.~ (x~z) \right)\\ &=\left(\lambda x ~.~ (z) \right) \\&= \underbrace{\left(\lambda x ~.~z \right)}_{\text{ret val is always }z } \\&= \left(\lambda z ~.~z \right) \\ \therefore~\left(\lambda x ~.~ (x~z) \right)&=\left(\lambda z ~.~z \right) \end{align}$$

Is this conclusion correct?

Answer 1

The term $(\lambda x. (x z))$ is not $\beta$-reducible, because there is never the situation $(\lambda \xi. a) b$ (where $\xi$ stands for any variable and $a,b$ for any terms). So it is in normal form and cannot be simplified further.

In this term (and without further context), the symbols $x, z$ do not stand for other terms, but they are "just" syntactic symbols. There is no need to talk about "independence".

In your sequence of equations the second and the fourth equality are wrong. The first function says: "I'll take an input and apply it to $z$." The second says: "I'll take an input, forget about it and return $z$." And the third says: "I'll take an input and return it again."

Notice what happens, when these functions are evaluated on different inputs:

• $(\lambda x. (x z))(\lambda y.y) =_\beta (\lambda y.y) z =_\beta z$
• $(\lambda x. z)(\lambda y.y) =_\beta z$
• $(\lambda z. z)(\lambda y.y) =_\beta (\lambda y. y)$

For the sake of illustration, let's allow numbers and addition in our language. Then we can compute more examples:

• $(\lambda x. (x z))(\lambda y.y+1) =_\beta (\lambda y.y+1) z =_\beta z+1$
• $(\lambda x. z)(\lambda y.y+1) =_\beta z$
• $(\lambda z. z)(\lambda y.y+1) =_\beta (\lambda y. y+1)$

In all these computations the last term is in normal form.