0
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ So my problem was understanding the capture, can you, please, give me an example of a β-reduction where substitution is needed? $\endgroup$ – geckos Nov 8 '20 at 12:42
  • $\begingroup$ @geckos I added an example. $\endgroup$ – lemontree Nov 8 '20 at 12:53
  • $\begingroup$ Thanks for your help @lemontree it is very helpful :) $\endgroup$ – geckos Nov 8 '20 at 16:01
  • $\begingroup$ 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? $\endgroup$ – geckos Nov 8 '20 at 16:12
  • $\begingroup$ I updated the question with more information on the alpha notation doubts I hope I'm not bothering :) $\endgroup$ – geckos Nov 8 '20 at 17:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.