What are free variables in lambda calculus?

Question

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?

Basically, the $\lambda$ operator is the only one binding variables. — Mauro ALLEGRANZA, Jul 19 '22 at 07:38
I understand syntax and how we bind free variables. My understanding breaks when I see .. How to make a program out of it? Is it useful only to make closed term later? — Oleg Dats, Jul 19 '22 at 07:44
In general, fro Church encoding, the lack of free var seems correct... "numerals" are the usual names for numbers: $0,1=s(0), 2=s(1), \ldots$ and they have no free variables. — Mauro ALLEGRANZA, Jul 19 '22 at 07:46
Can you please provide an example where we need free variables? — Oleg Dats, Jul 19 '22 at 08:27
Where we use it... See Lambda terms: "The abstraction $\lambda x.x+y$ is syntactically valid, and represents a function that adds its input to the yet-unknown $y$." — Mauro ALLEGRANZA, Jul 19 '22 at 08:41
How to think of it as a computable function? Is it possible to construct a Turing machine or SKI combinator term for this term? Can we assign a type for this term? — Oleg Dats, Jul 19 '22 at 08:49

score 4 · Accepted Answer · answered Jul 19 '22 at 07:46

4

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$.

answered Jul 19 '22 at 07:46

Captain Lama

25,743

So $y$ is like a name for another term. In Haskell it will be: let y = \x->x+1, (\x->y x) 2 = 3? It implies that it is impossible to convert . to SKI combinators because we do not know $y$? – Oleg Dats Jul 19 '22 at 08:38
@OlegDats: The word "combinator," in the context of the lambda calculus, literally means "a lambda expression that does not have any free variables." – Kevin Jul 19 '22 at 15:45
"In the above example, the expression [x].xy is not itself a CL-term, but is merely a short-hand to denote the CL-term SI(Ky)." I know that Combinators is a subset of CL-terms. It was helpful for me know how free variables are represented in CL. – Oleg Dats Jul 21 '22 at 16:27

score 0 · Answer 2 · answered Mar 30 '24 at 07:28

Free variables can always be regarded as being bound in a larger context containing the one you're looking at. So $y(λx·xy)$ could just as well be considered as being inside the context $C = λy·y(λx·xy)$, and the term, itself, can be considered as a template $$y(λx·xy) = (λy·y(λx·xy))y = Cy,$$ where the "$y$" in "$Cy$" can stand for anything and $C$ has no free variables.

If you don't have free variables, then you're seriously hampering your ability to talk about sub-contexts of contexts, and sub-terms of terms, without treating contexts and terms as black boxes.

It's a case of the general situation where discussion of $A$ is much easier and more natural when done as discussion of $A$ and $B$ together, rather than of $A$ alone, even where $B$ may not have the same kind of meaningfulness as $A$. That situation happens all the time in mathematical analysis, and that's what invariably drives discussion toward abstractions like $B$ from things more concrete like $A$. The situation, itself, is telling you that you need to talk about $B$, too, and to not limit attention to just $A$ on "pragmatism" grounds. It's the kind of case where pragmatism is impractical.

What are free variables in lambda calculus?

2 Answers2