What is the least general computable property that all non-terminating redexes have in common?

133 Views Asked by At

The simplest example of a non-terminating reducible expression is ((λx. x x) (λx. x x)), which $\beta$-reduces to itself in one step and is therefore non-terminating.

This also highlights a class of non-terminating redexes: those that $\beta$-reduce to themselves in one step obviously do not terminate.

But I am interested in the determining whether this process ever ends for any arbitrary redex ((λx.y) z).

Do all non-terminating redexes eventually reach a point where they $\beta$-reduce to themselves in one step, or are there other classes of non-terminating redexes as well?

Specifically, I am looking for general properties that all non-terminating redexes have in common, even if the property is not exclusive to non-terminating redexes; e.g., is the argument, z, always an abstraction for non-terminating redexes?

1

There are 1 best solutions below

8
On

Computational capabilities of lambda calculus are the same to capabilities of Turing machines, i.e. we can perform beta reduction using Turing machine and also we can simulate Turing machine with some lambda expression. Therefore if it is possible to determine if beta reduction terminates, we can translate an arbitrary Turing machine to lambda expression and check if beta reduction terminates which is equivalent to halting problem. So if by words “determining if beta reduction terminates” you mean building an algorithm for Turing machine to determine in finite amount of time if beta reduction terminates, the answer would be it is impossible.