I am having trouble understanding the concept of free variables in lambda calculus.
How and when should we use them?
I read all Church encoding and there is no use of free variables. Natural numbers, arithmetic, pairs… everything is defined without free variables.
It is also unclear how to translate the lambda term with free variables into programming languages. For example $𝜆x.yx$. What is $y$? For $𝜆yx.yx$ everything is clear. It is just $f(x)$. Meaning the lambda term takes 2 parameters and applies the first one to the second one. What is the meaning of $𝜆x.yx$?
In computer programming, the term free variable refers to variables used in a function that are neither local variables nor parameters of that function. wiki
What does it mean? Is it a global function?
Best Answer
The term $\lambda x. yx$ is equivalent to just $y$. In mathematical notation it is the function $x\mapsto y(x)$, which is just... the function $y$. To the question "what is $y$", there is no better answer than... it is $y$. Whatever $y$ is. It's some $\lambda$-term represented by a variable, which in this case is $y$.
On the other hand note that contrary to what you say, $\lambda yx. yx$ does not represent $y(x)$ (or $f(x)$ as you write it, but it seems a bad idea to use another letter randomly), but rather the function $(y,x)\mapsto y(x)$. To represent $y(x)$ as a $\lambda$-term, you just write $yx$.