# 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.

• Equivalent in what sense? $\beta$-equivalence? A form of contextual equivalence? – Rodolphe Lepigre Dec 19 '18 at 12:14
• @RodolpheLepigre Equivalent using alpha, beta, and eta conversions. – PyRulez Dec 19 '18 at 14:30
• Just to clarify, could you describe what the reduction you have in mind for $\Omega\ v$ is? – cody Jan 22 '19 at 14:04
• @cody Whoops, that example does not work. I changed it to $\Omega ((\lambda a.b. a) \Omega v)$, which reduces to $\Omega \Omega$. – PyRulez Jan 22 '19 at 18:14

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.

• 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. – PyRulez Dec 20 '18 at 14:19