Editing Rice's theorem (section)

===Formal proof===
[[Image:Rice reduction.svg|thumb|If we have an algorithm that decides a non-trivial property, we can construct a Turing machine that decides the halting problem.]]

For the formal proof, algorithms are presumed to define partial functions over [[string (computer science)|strings]] and are themselves represented by strings. The partial function computed by the algorithm represented by a string ''a'' is denoted '''F'''<sub>''a''</sub>. This proof proceeds by [[reductio ad absurdum]]: we assume that there is a non-trivial property that is decided by an algorithm, and then show that it follows that we can decide the [[halting problem]], which is not possible, and therefore a contradiction.

Let us now assume that ''P''(''a'') is an algorithm that decides some non-trivial property of '''F'''<sub>''a''</sub>. Without loss of generality we may assume that ''P''(''no-halt'') = "no", with ''no-halt'' being the representation of an algorithm that never halts. If this is not true, then this holds for the algorithm ''{{overline|P}}'' that computes the negation of the property ''P''. Now, since ''P'' decides a non-trivial property, it follows that there is a string ''b'' that represents an algorithm '''F'''<sub>''b''</sub> and ''P''(''b'') = "yes".  We can then define an algorithm ''H''(''a'', ''i'') as follows:

:1. construct a string ''t'' that represents an algorithm ''T''(''j'') such that
:* ''T'' first simulates the computation of '''F'''<sub>''a''</sub>(''i''),
:* then ''T'' simulates the computation of '''F'''<sub>''b''</sub>(''j'') and returns its result.
:2. return ''P''(''t'').

We can now show that ''H'' decides the halting problem:
* Assume that the algorithm represented by ''a'' halts on input ''i''. In this case '''F'''<sub>''t''</sub> = '''F'''<sub>''b''</sub> and, because ''P''(''b'') = "yes" and the output of ''P''(''x'') depends only on '''F'''<sub>''x''</sub>, it follows that ''P''(''t'') = "yes" and, therefore ''H''(''a'', ''i'') = "yes".
* Assume that the algorithm represented by ''a'' does not halt on input ''i''. In this case '''F'''<sub>''t''</sub> = '''F'''<sub>''no-halt''</sub>, i.e., the partial function that is never defined. Since ''P''(''no-halt'') = "no" and the output of ''P''(''x'') depends only on '''F'''<sub>''x''</sub>, it follows that ''P''(''t'') = "no" and, therefore ''H''(''a'', ''i'') = "no".

Since the halting problem is known to be undecidable, this is a contradiction and the assumption that there is an algorithm ''P''(''a'') that decides a non-trivial property for the function represented by ''a'' must be false.