# Lambda Calculus and naming

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?

• In lambda calculus everything is just a character. Nothings is defined or stands for anything. The lambda expressions can be ‘applied’ to other lambda terms, but that is just concatenation. Reduction then is just a process of substitution. Everything is syntax. – Ittay Weiss Apr 2 '18 at 17:58
• The little you have written does not tell us what $y$ and $z$ are. They might have less than "global" scope, but it is possible that they do have that. I think it might be easier to work with a more complete example to explain scoping. See for example the previous Question "How do scoping rules work in the Lambda Calculus with nested functions". – hardmath Apr 2 '18 at 17:59
• @IttayWeiss Is the thing I wrote, $(\lambda x.yx)z \implies yz$, also a valid $\lambda$-term? I can see that everything is a character but I understood that those should occur in a $\lambda$-abstraction, am I wrong? – meguli Apr 2 '18 at 18:11
• @meguli these are two lambda terms. The implication arrow is not part of the lambda calculus syntax. It indicates that the term on the right is obtained from the term,on the left by the rules of manipulation of lambda terms. – Ittay Weiss Apr 2 '18 at 19:15
• – ljedrz Apr 2 '18 at 21:19