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

Question

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 :)

Answer 1

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.