Lambda Calculus and naming

222 Views Asked by At

I see that $\lambda$-calculus let's you work with anonymous functions and names are purely local. As an example

$$\lambda x.x$$

contains $x$ only as a local name. This will be replaced during reduction by another anonymous $\lambda$-term. So, I am seeing examples like

$$(\lambda x.yx)z \implies yz$$

But what is $y$ and $z$? Are these referring to other global names that we have defined before, they are not bound in any $\lambda$-term so they are free. But, to what they refer to? Did we name them in some way? What is the mechanism for naming global things and how this works with bare $\lambda$-calculus?