Fix an acceptable effective enumeration of the -ary partial computable functions. The S-m-n theorem states that for every there is a total computable function such that
where means that both sides have the same value when defined and are otherwise both undefined.
The recursion theorem states that every total computable transformation of program indices has a semantic fixed point: there is an such that
Rice theorem says that every nontrivial extensional property of programs computing partial functions is undecidable. Equivalently, a nontrivial index set cannot be a computable set.
Let be such an index set. Replacing by its complement if necessary, assume that the nowhere-defined function has no index in . Since the property is nontrivial, choose an index . If membership in were decidable, we could decide the diagonal halting problem as follows. For each , define
By the S-m-n theorem, a total computable function produces an index for . If diverges, then is nowhere defined and . If it halts, then and extensionality gives . A decider for would therefore decide whether halts, a contradiction. Hence is undecidable.
Apply the S-m-n theorem to . It gives a total computable function such that
The recursion theorem supplies an index satisfying . Consequently
For each , let be an effectively obtained index of the partial function
The existence of the total computable index transformation follows from the S-m-n theorem. By the recursion theorem, some satisfies . Therefore its domain is
and hence
No. The property
is an index set: it depends only on the domain of the partial function computed, not on the syntax of its program. It is nontrivial. For example, an index whose domain is a singleton belongs to , whereas an index whose domain has two elements does not. The Rice theorem therefore shows that is not a computable set, so no algorithm can decide the requested property for arbitrary .
Invoking the Church–Turing thesis, this also rules out any effective procedure in the informal sense, because such a procedure would be represented by a computable function.

Articles by others on the same topic (0)

There are currently no matching articles.