Efficient algorithm to determine if a lambda calculus term is equivalent to one without a given free variable

Question

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.

• Rodolphe Lepigre: Equivalent in what sense? $\beta$-equivalence? A form of contextual equivalence?
• Christopher King: @RodolpheLepigre Equivalent using alpha, beta, and eta conversions.
• cody: Just to clarify, could you describe what the reduction you have in mind for $\Omega\ v$ is?
• Christopher King: @cody Whoops, that example does not work. I changed it to $\Omega ((\lambda a.b. a) \Omega v),ドル which reduces to $\Omega \Omega$.

Answer 1

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)

• Christopher King: That is only worst case.
• chi: @PyRulez Correct. So, to make the problem interesting, we have to specify what kind of notion of "efficient" we have in mind.
• Christopher King: Hmm, I thought about it a little, and edited the question with what I think is a suitable notion of efficiency.
• chi: I think that my answer is already compatible with your notion, proving that no efficient (as per your definition) algorithm can exist.
• Christopher King: I think with my new definition, your proof of decidability is now incorrect. $g(n)$ will be undefined if $\phi(t,v)$ is false (since then $n$ will be undefined), making the algorithm incorrect.