Definition of variable V occurring free in lambda expression E

Question

What does the following mean?

$$ (\lambda V_1 V_2.E) E_1 E_2 $$

"$V_2$ occurs free in $E_1$."

Does this mean $E_1$ contains references to $V_2$?

Could you explain with examples? Thanks a bunch!

Answer 1

Thank you to @PlanckWalk from libera #math.

Let's consider

$$ (\lambda v_1. \lambda v_2. \underline{sum})(\lambda w. v_2+1)(\underline{3}) $$

Here, $v_2$ occurs free in $(\lambda w. v_2 +1)$.

That's what it means.

Relatedly, substitution $E[E'/V]$ is invalid if any free variable in $E'$ gets bound in $E[E'/V]$.

For example,

$$ (\lambda w. \lambda v. \underline{sum} \ w)(\lambda w.v) = (\lambda v. \underline{sum} \ w)[(\lambda w. v)/w] = (\lambda v. \underline{sum} \ \lambda w. v) $$

is invalid because free variable $v$ in $(\lambda w. v)$ gets bound in $\underline{sum}$.

Even simpler

$$ (\lambda v. \lambda w. v)(w) = (\lambda w. v)[w/v] = (\lambda w. w) $$

is also invalid since free $w$ gets bound in $(\lambda w.w)$.