Consider the following problem: given a lambda calculus term $t$ and free variable $v$ determine whether $\phi(t,v)$, where $\phi(t,v) := \exists t'. t' \equiv t \land v \notin FV(t')$.
This problem is undecidable. To prove this, assume the contrary. We define a term $s$ as follows:
$$s x \equiv \lambda n.j. j y$$
if $x$ is an encoding of the configuration of a Turing machine and $y$ is the encoding of the configuration the Turing machine transitions into in one step and
$$s x \equiv \lambda n.j. n$$
if $x$ is an encoding of the configuration of a Turing machine that has halted.
Now define the term $t_M$ as follows:
$$t_M := Y (\lambda f.x. s x (\lambda a.b. b) f) i_M$$
where $i_M$ is the encoding of the initial configuration of $M$, and $Y$ is the fixed point combinator.
If $M$ halts, $t_mv \equiv (\lambda b. b)$. Otherwise, $t_mv$ does not have a normal form, and every term equivalent to it has $v$ in it. Therefore, $\phi(t, v)$ iff $M$ halts. This algorithm can be used to solve the halting problem, which is a contradiction.
On the other hand, it is semidecidable. For any $t$ and $v$, simply enumerate the $t'$ such that $t' \equiv t$. If a $t'$ is enumerated such that $v \notin FV(t')$, output yes and halt. This algorithm outputs yes iff $\phi(t, v)$.
That said, this algorithm is not very efficient, since you have to use an enumeration that enumerates all $t'$ such that $t' \equiv t$. Is there an efficient algorithm to semidecide whether $\phi(t,v)$ is true?
EDIT: We'll say an algorithm for determining $\phi(t,v)$ is efficient if, when $\phi(t,v)$ is true, it halts in an amount of time that is a polynomial of the minimum number of reduction and conversion steps required to eliminate $v$ from $t$.
An approach one might consider is to normalize $t$, and then check if $v$ is free in the result. Although this would be efficient, it would not be correct. For example, this algorithm would not halt on the input $(\Omega ((\lambda a.b. a) \Omega v), v)$ (where $\Omega := (\lambda x. x x)(\lambda x. x x)$), but $\phi(\Omega ((\lambda a.b. a) \Omega v), v)$ is true.
Another approach would be to use some reduction strategy, and then to check after each step if $v$ is free in the term produced by that step. Although I think this is a good direction to take, it should be noted that neither normal order reduction nor applicative order reduction would work. To see this, consider the input $(t_M(t_Nv),v)$. If $M$ diverges but $N$ halts, $\phi(t_M(t_Nv),v)$ is true, but normal order reduction will never eliminate $v$. Likewise, if $M$ halts but $N$ diverges, $\phi(t_M(t_Nv),v)$ is again true, but applicative order will never eliminate $v$.
The input $(t_M(t_Nv),v)$ is rather tricky in general. To solve this input, an algorithm would probably need to attempt to normalize $t_M$ and $t_N$ in parallel, outputting yes if either normalizes. Attempting to normalize $t_M$ first or normalize $t_N$ first will not work.
On the other hand, by the Church-Rosser theorem, we only need reductions, no expansions. We never need to "undo" a reduction step to eliminate a variable. That is because if $t' \equiv t \land v \notin FV(t')$, there is some term that both $t$ and $t'$ reduce to. It will not contain $v$, since $t'$ does not, and reductions never introduce free variables. Since $t$ also reduces to this term, $t$ can be reduced to a term without $v$.
Alpha conversion does not make a difference. It appears that eta conversion is also irrelevant.
