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. For any Turing machine $ M$ , let $ t_M$ be a lambda calculus term that normalizes to $ \lambda x. x$ if $ M$ halts and diverges otherwise. Then determine whether $ \phi(t_M(\lambda x. (\lambda y. y))v, v)$ . If it is true, then $ M$ halts. Otherwise, it does not. This provides an algorithm 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 determine whether $ \phi(t,v)$ is true?
One thing one might consider is to normalize $ t$ , and then determine whether $ v$ is a free variable in the normal form of $ t$ . Although this is efficient, it is not correct. Consider the term $ t := \Omega((\lambda x. \lambda y. x)\Omega v)$ (where $ \Omega := (\lambda x. x x)(\lambda x. x x)$ ). $ t$ does not have a normal form. Yet, $ \phi(t,v)$ is true, since $ (\Omega \Omega) \equiv t \land v \notin FV(\Omega \Omega)$ .
Note also that normalizing $ t$ using and checking if $ v$ is free in the intermediate terms after each step will not work if one uses normal-order reduction or applicative order reduction. The counterexample for both is $ \phi(\Omega((\lambda x. \lambda y. x)\Omega v), v)$ , the same as before.
One approach would be to find some other efficient reduction strategy (perhaps depending on $ v$ ) that will eventually produce a term that does not contain $ v$ , if such a term exists. This potentially could solve $ \phi(\Omega((\lambda x. \lambda y. x)\Omega v), v)$ , since $ \Omega((\lambda x. \lambda y. x)\Omega v)$ can be reduced to $ \Omega((\lambda y. \Omega) v)$ which can be reduced to $ \Omega \Omega$ , which does not contain $ v$ . We need a strategy that works on arbitrary $ t$ though.
Alpha conversion does not make a difference. It appears that eta conversion is also irrelevant.