Is there a systematic way to know when to alpha-transform free variables?

So, using Church numerals, we define

$3 = {\lambda} f. {\lambda}x.f(f(f(x)))$,

and

$4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$.

We can then add with an expression like

$3\ g\ (4\ g\ z)$

And this reduces to:

$(g (g (g (g (g (g (g\ z)))))))$

... but why?

$g$ is a free variable in each expression, and my understanding is that you must ${\alpha}$-convert free standing variables in unrelated expressions. Shouldn't we instead end up with something like

$(g (g (g (g_2 (g_2 (g_2 (g_2\ z)))))))$?

The answer here is the same as in the other question: one thing is missing here!

Your addition result should be:

$$3 + 4 = \lambda g . \lambda z . 3 g (4 g z) = \lambda g . \lambda z . 7 g z$$

Note that $g$ is now a lambda parameter, not a free variable! So now if you want to apply this to something, it'll get substituted in the same everywhere:

$$7 q r = (\lambda g . \lambda z . 7 g z) q r = q q q q q q q r$$

StackExchange Computer Science Q#103476, answer score: 5