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.

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

1 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)

  • $\begingroup$ That is only worst case. $\endgroup$ Commented Dec 19, 2018 at 19:05
  • $\begingroup$ @PyRulez Correct. So, to make the problem interesting, we have to specify what kind of notion of "efficient" we have in mind. $\endgroup$
    – chi
    Commented Dec 19, 2018 at 19:08
  • $\begingroup$ Hmm, I thought about it a little, and edited the question with what I think is a suitable notion of efficiency. $\endgroup$ Commented Dec 20, 2018 at 14:13
  • $\begingroup$ I think that my answer is already compatible with your notion, proving that no efficient (as per your definition) algorithm can exist. $\endgroup$
    – chi
    Commented Dec 20, 2018 at 14:15
  • $\begingroup$ 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. $\endgroup$ Commented Dec 20, 2018 at 14:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.