patternMinor
Efficient algorithm to determine if a lambda calculus term is equivalent to one without a given free variable
Viewed 0 times
withoutequivalentcalculusfreeefficienttermalgorithmonedeterminevariable
Problem
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)$ (wher
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)$ (wher
Solution
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)
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)
Context
StackExchange Computer Science Q#101767, answer score: 2
Revisions (0)
No revisions yet.