# Is (λx.FV(A)) and (λx.FV(B)) β-equivalent?

Does free variables have some meaning in lambda calculus? If I follow this β-reduction

(λx.λz.y x) y
-> (λz.y x){x/y}        (variable FV(y) captured)
-> ((λz.y x){a/y}){x/y} (rename FV(y) -> FV(a)){
-> (λz.a x){x/y}
-> (λz.a y)


Here we have FV(y) captured during the β-reduction, so I rename it to FV(a) and continue the reduction. Is this result even valid?

I would rename the y argument instead

(λx.λz.y x) y
-> (λz.y x){x/y}        (variable FV(y) captured)
-> (λz.y x)({x/y}{y/a}) (rename argument FV(y) -> FV(a)
-> (λz.y x){x/a}
-> (λz.y a)


If I use De Bruijin index notation for both outputs I would get:

(λz.a y) -> (λ.1 2)
(λz.y a) -> (λ.1 2)


so they seem β-equivalent for me.

This means that FV has no meaning at all, FV(a) β= FV(b) β= FV(c) ...  is my understanding right?

I'm asking because when applying lambda calculus I would like to have some global variables that are not bound by the expression but are bound by the context, things like *, +, sqrt, etc, in this case I cant just replace free variables because they may have a meaning, what would I do so?

Thanks @lemontree for your answer, I'm implementing a lambda calcualtor so I need to take care of every single step. I write things in the math notation (λx.x) y and then translate to the expected code Appl(Lamb('x', 'x'), 'y'), M[x/y] m.replace('x', 'y'), so having a notation for every step help me a lot :).

I search but can't find any special notation for ɑ-conversion so I came up with M[BV(x)/y] to denote that x is not free in M and to make it distinct from M[x/y]. And a special function NX that returns the next available variables. Here is how I reduced your example (thank you!)

    (λx.λy.y x) y
-> (λy.y x)[y/x]
-> (λy.y[y/x] x[y/x])               CAPTURE ERROR on y (backtrack)
-> (λy.y x)[BV(y)/NX(x, y)][y/x]    NX(FV ∪ BV) returns the next available variable
-> (λy.y x)[BV(y)/z][y/x]
-> (λz.z x)[y/x]
-> (λz.z[y/x] x[y/x])
-> (λz.z y)


The bits that I missed

• A definition of available variables not (FV ∪ BV). I need this to implement ɑ-conversion
• A formal notation for ɑ-conversion

Is there anything like this in the literature? Thanks in advance :)

Free variables have a "meaning" in the sense that two free variables (as opposed to two bound variables) are not $$\alpha$$-equivalent -- and that's precisely why your first reduction is not correct: We are not allowed to do "free renaming", only bound renaming!

Capture avoiding substitution is defined as

If $$x \neq y$$ and $$y \in FV(N)$$ and $$x \in FV(P)$$, then, where $$z \not \in FV(N) \cup FV(P)$$: $$(\lambda y.P)[N/x] = \lambda z.(P[z/y][N/x])$$

Capture avoiding substitution happens only when a variable occurring free in $$N$$ is bound by lambda abstraction in the term to substitute ($$y \in FV(N)$$) and there are actual occurrences of $$x$$ in $$P$$ to substitute ($$x \neq y$$ and $$x \in FV(P)$$). In that case, we rename the bound variable in the term that undergoes substitution (the function body), i.e. $$(\lambda y.P) \rightsquigarrow \lambda z. (P[z/y])$$, then perform the actual substitution of $$N$$ for $$x$$ in $$P'$$. We do not rename free variables, and we do not perform renaming in the argument.

In your example, beta-reducing $$(λx.λz.y x) y$$ means to replace every free occurrence of $$x$$ in $$\lambda z. yx$$ by $$y$$ provided that $$y$$ is free to substitute. y will not be captured by anything: As you observe, $$y$$ is free in $$\lambda z.yx$$, and that's precisely why there is no capturing and thus no capture avoiding to perform, and the substitution can be done directly. Thus the correct reduction is

$$\newcommand{\bred}{\triangleright_\beta} \phantom{\triangleright_\beta} (\lambda x. \lambda z. yx)y\\ \bred (\lambda z.yx)[y/x]\\ = \lambda z. (yx[y/x])\\ = \lambda z. (y[y/x])(x[y/x])\\ = \lambda z. yy$$

De Bruijn indexing on this term is vacuous, because there are no pairs of binding and bound variables ($$\lambda z$$ does not bind any occurrences of $$z$$, and the two occurrences of $$y$$ are not bound by any abstraction $$\lambda y$$).

A case where capture avoiding substitution would be needed is if the argument $$y$$ were bound in the function body, e.g. if instead of the vacuous abstraction $$\lambda z$$ there were $$\lambda y$$:

$$(\lambda x. \lambda y. yx)y\\ \bred (\lambda y.yx)[y/x]\\ = \lambda z. (yx[z/y][y/x]) \quad \text{(avoiding catpure of y)}\\ = \lambda z. (zx[y/x])\\ = \lambda z. zy$$

Re. notation and implementation:

It depends a bit on how you define it, but the way I used it above (which is the approach chosen in e.g. Hindley & Seldin (see below):
When bound renaming has to happen to avoid variable capture, then this is part of the definition of substitution, i.e. the result of $$(\lambda y.P)[N/x]$$ with $$y$$ free in $$N$$ syntactically identical ("$$=$$", rather than just $$\alpha$$-equivalent) to $$\lambda z.P[z/y][N/x]$$.
To express $$\alpha$$-equivalence in the sense that a pair of terms only differs in their bound variable names, you can write $$\equiv_\alpha$$.
Alternatively, one could define beta reduction such that substitution can only be performed if no variable conflict occurs, and if it does, one has to prepend a step of $$\alpha$$-renaming before $$\beta$$-reducing.

"not $$FV(A) \cup FV(B)$$" is just the set-theoretic complement relative to the set of all variables, $$VAR - (FV(A) \cup FV(B))$$. To implement a choice of "the first variable not in $$FV(A) \cup FV(B)$$" you need to presuppose an ordering of variables such as $$x < y < z < x_1 < ... x_n$$ and then do something like $$min\{x: x \in VAR \land x \not \in FV(A) \land x \not \in FV(B)\}$$. The set of free and bound variables is defined by straightforward recursion on the structure of the lambda term.

Furthermore, for a precise notation in the implementation one may want to distinguish between an atomic beta reduction/variable renaming step vs. reducibility/equivalence through a chain of reductions/renamings, as well as $$\beta$$-reducibility monotonously downwards from $$A$$ to $$B$$ as opposed to $$\beta$$-equivalence by finding a common term both reduce to.

For variables you should use $$x, y, z, u, v, w, x_1, x_2, \ldots$$; wheras $$a, b, c, \ldots$$ are more typically understood as constants.
Constants is also what objects and functions interpreted "by context" such as $$*, +, sqrt$$ would naturally be treated as; their meaning is "fixed from the outside" and you can combine lambda reduction with custom inference steps like $$(\lambda x.+xx)(2) \bred +22 =_\mathbb{N} 4$$.

You can find the notation I used and all the definitions necessary for rigorously implementing substitution etc. in (amongst others)

J. R. Hindley & J.P. Seldin (2008), Lambda calculus and combinators: an introduction.

Another classic is

H. Barendregt (1992), Lambda calculi with types.

• So my problem was understanding the capture, can you, please, give me an example of a β-reduction where substitution is needed? – geckos Nov 8 '20 at 12:42
• @geckos I added an example. – lemontree Nov 8 '20 at 12:53
• Thanks for your help @lemontree it is very helpful :) – geckos Nov 8 '20 at 16:01
• As a last question, is there any notation for ɑ-conversion? Something like (λx.x)[z/x] = (λz.z), I know that M[z/x] usually means replace all free x by z but in this case x is not free, is there any special notation for that? – geckos Nov 8 '20 at 16:12
• I updated the question with more information on the alpha notation doubts I hope I'm not bothering :) – geckos Nov 8 '20 at 17:10