Efficient algorithm to determine if a lambda calculus term is equivalent to one without a given free variable 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.
You can't semi-decide a non decidable problem in an efficient way.

Suppose that you have an algorithm $A$ which semidecides such a problem in, say, $T(n)$. I.e. every word in the problem is accepted within $T(n)$ steps. Assume that $T(n)$ is bounded from above by any computable total function $g(n)$ (say $2^{2^n}$, which allows $A$ to range over any efficient algorithm).

Then, the problem is decidable: run $A$ for at most $g(n)$ steps, and accept if $A$ accepts, otherwise reject.

Contradiction. QED

Asymptotically, a semidecider of a non recursive problem can never be efficient. (Unless we choose another definition of "efficient" than "low worst-case complexity", I guess)